Function vstd::arithmetic::power::lemma_pow_increases
source · pub broadcast proof fn lemma_pow_increases(b: nat, e1: nat, e2: nat)Expand description
requires
b > 0,e1 <= e2,#[trigger] pow(b as int, e1) <= #[trigger] pow(b as int, e2),Proof that a positive number raised to a power increases as the
power increases. Specifically, since e1 <= e2, we know pow(b, e1) <= pow(b, e2).