Function vstd::arithmetic::power::lemma_pow_increases_converse

source · 
pub broadcast proof fn lemma_pow_increases_converse(b: nat, e1: nat, e2: nat)
Expand description
requires
1 < b,
#[trigger] pow(b as int, e1) <= #[trigger] pow(b as int, e2),
ensures
e1 <= e2,

Proof that if the exponentiation of a number greater than 1 doesn’t decrease when the exponent changes, then the change isn’t a decrease. Specifically, given that b > 1 and pow(b, e1) <= pow(b, e2), we can conclude that e1 <= e2.