vstd::arithmetic::power

Function lemma_pow_mod

Source 
pub broadcast proof fn lemma_pow_mod(b: nat, e: nat)
Expand description
requires
b > 0,
e > 0,
ensures
#[trigger] pow(b as int, e) % b as int == 0,

Proof that pow(b, e) modulo b is 0.