Function vstd::arithmetic::power::lemma_pow_strictly_increases_converse

b > 0,

#[trigger] pow(b as int, e1) < #[trigger] pow(b as int, e2),

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.