Function vstd::arithmetic::power::lemma_pow_multiplies

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

Function vstd::arithmetic::power::lemma_pow_multipliesCopy item path