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