Function vstd::arithmetic::power::lemma_pow_subtracts
source · pub broadcast proof fn lemma_pow_subtracts(b: int, e1: nat, e2: nat)Expand description
requires
b > 0,e1 <= e2,pow(b, e1) > 0,#[trigger] pow(b, (e2 - e1) as nat) == pow(b, e2) / pow(b, e1) > 0,Proof that, as long as e1 <= e2, taking a positive integer b
to the power of e2 - e1 is equivalent to dividing b to the
power of e2 by b to the power of e1.