Function vstd::arithmetic::power::lemma_pow_strictly_increases_converse

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

Proof that if an exponentiation result strictly increases when the exponent changes, then the change is an increase. Specifically, if we know pow(b, e1) < pow(b, e2), then we can conclude e1 < e2.