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