Function vstd::arithmetic::mul::lemma_mul_cancels_negatives

source · 
pub broadcast proof fn lemma_mul_cancels_negatives(x: int, y: int)
Expand description
ensures
#[trigger] (x * y) == (-x) * (-y),

Proof that multiplying -x and -y produces the same product as multiplying x and y