vstd::arithmetic::power

Function lemma_pow0

Source
pub broadcast proof fn lemma_pow0(b: int)
Expand description
ensures
#[trigger] pow(b, 0) == 1,

Proof that the given integer b to the power of 0 is 1.