Function vstd::arithmetic::mul::lemma_mul_cancels_negatives

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

Function vstd::arithmetic::mul::lemma_mul_cancels_negativesCopy item path