Function vstd::arithmetic::power::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