Function vstd::arithmetic::power::lemma_pow_multiplies
source · pub broadcast proof fn lemma_pow_multiplies(a: int, b: nat, c: nat)Expand description
ensures
0 <= b * c,#[trigger] pow(pow(a, b), c) == pow(a, b * c),Proof that a to the power of b * c is equal to the result of
taking a to the power of b, then taking that to the power of
c