proposition: Lemma negate_zero_prod_r x y : x * -y = 0 ↔ x * y = 0.
proof: Proof. rewrite (commutativity x (-y)), (commutativity x y). apply negate_zero_prod_l. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra