vstd::arithmetic::mul

Function lemma_mul_is_commutative

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

Proof that multiplication is commutative, specifically that x * y == y * x.