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),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.