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,#[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.