Function vstd::arithmetic::power::lemma_pow_sub_add_cancel
source · pub broadcast proof fn lemma_pow_sub_add_cancel(b: int, e1: nat, e2: nat)Expand description
requires
e1 >= e2,#[trigger] pow(b, (e1 - e2) as nat) * pow(b, e2) == pow(b, e1),Proof that if e1 >= e2, then b to the power of e1 is equal
to the product of b to the power of e1 - e2 and b to the
power of e2