vstd::arithmetic::power

Function lemma_square_is_pow2

Source 
pub broadcast proof fn lemma_square_is_pow2(x: int)
Expand description
ensures
#[trigger] pow(x, 2) == x * x,

Proof that taking the given number x to the power of 2 produces x * x.