lemma_log_pow

vstd::arithmetic::logarithm

Function lemma_log_pow 

Source 
pub proof fn lemma_log_pow(base: int, n: nat)
Expand description
requires
base > 1,
ensures
log(base, pow(base, n)) == n,

Proof that the integer logarithm of pow(base, n) in base base is n.