pub broadcast proof fn lemma_pow1(b: int)
#[trigger] pow(b, 1) == b,
Proof that the given integer b to the power of 1 is b.
b