Function vstd::arithmetic::power::lemma_pow_mod_noop

source ·

pub broadcast proof fn lemma_pow_mod_noop(b: int, e: nat, m: int)

Expand description

requires

m > 0,

ensures

#[trigger] pow(b % m, e) % m == pow(b, e) % m,

Proof that exponentiation then modulo produces the same result as doing the modulo first, then doing the exponentiation, then doing the modulo again. Specifically, ((b % m)^e) % m == b^e % m.