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