vstd::arithmetic::logarithm

Function lemma_log_nonnegative

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

Proof that the integer logarithm is always nonnegative. Specifically, log(base, pow) >= 0.