Function vstd::arithmetic::power::lemma_pow1

source · 
pub broadcast proof fn lemma_pow1(b: int)
Expand description
ensures
#[trigger] pow(b, 1) == b,

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