Function vstd::arithmetic::logarithm::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