Function vstd::arithmetic::power::lemma_pow_strictly_increases
source · pub broadcast proof fn lemma_pow_strictly_increases(b: nat, e1: nat, e2: nat)Expand description
requires
1 < b,e1 < e2,#[trigger] pow(b as int, e1) < #[trigger] pow(b as int, e2),Proof that a number greater than 1 raised to a power strictly
increases as the power strictly increases. Specifically, given
that b > 1 and e1 < e2, we can conclude that pow(b, e1) < pow(b, e2).