pub broadcast proof fn lemma_mul_unary_negation(x: int, y: int)Expand description
ensures
(-x) * y == -(x * y) == x * (-y),Proof that negating x or y before multiplying them together
produces the negation of the product of x and y.