vstd::arithmetic::power

Function lemma1_pow

Source 
pub broadcast proof fn lemma1_pow(e: nat)
Expand description
ensures
#[trigger] pow(1, e) == 1,

Proof that 1 to the power of the given natural number e is 1.