Function vstd::arithmetic::mul::lemma_mul_unary_negation

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

Function vstd::arithmetic::mul::lemma_mul_unary_negationCopy item path