Function vstd::arithmetic::logarithm::lemma_log_is_ordered

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

Proof that since pow1 is less than or equal to pow2, the integer logarithm of pow1 in base base is less than or equal to that of pow2.