Function vstd::arithmetic::logarithm::lemma_log0

source · 
pub proof fn lemma_log0(base: int, pow: int)
Expand description
requires
base > 1,
0 <= pow < base,
ensures
log(base, pow) == 0,

Proof that since pow is less than base, its logarithm in that base is 0