pub broadcast proof fn lemma1_pow(e: nat)
#[trigger] pow(1, e) == 1,
Proof that 1 to the power of the given natural number e is 1.
e