Function vstd::arithmetic::power::lemma_pow_distributes
source · pub broadcast proof fn lemma_pow_distributes(a: int, b: int, e: nat)Expand description
ensures
#[trigger] pow(a * b, e) == pow(a, e) * pow(b, e),Proof that a * b to the power of e is equal to the product of
a to the power of e and b to the power of e