Function vstd::arithmetic::power::lemma_pow_adds
source · pub broadcast proof fn lemma_pow_adds(b: int, e1: nat, e2: nat)Expand description
ensures
#[trigger] pow(b, e1 + e2) == pow(b, e1) * pow(b, e2),Proof that taking an integer b to the power of the sum of two
natural numbers e1 and e2 is equivalent to multiplying b to
the power of e1 by b to the power of e2