Function vstd::arithmetic::logarithm::lemma_log_s

source · 
pub broadcast proof fn lemma_log_s(base: int, pow: int)
Expand description
requires
base > 1,
pow >= base,
ensures
pow / base >= 0,
log(base, pow) == 1 + log(base, pow / base),

Proof that since pow is greater than or equal to base, its logarithm in that base is 1 more than the logarithm of pow / base