Function vstd::arithmetic::power::lemma_pull_out_pows

source · 
pub broadcast proof fn lemma_pull_out_pows(b: nat, x: nat, y: nat, z: nat)
Expand description
requires
b > 0,
ensures
0 <= x * y,
0 <= y * z,
#[trigger] pow(pow(b as int, x * y), z) == pow(pow(b as int, x), y * z),

Proof that (b^(xy))^z = (b^x)^(yz), given that x * y and y * z are nonnegative and b is positive