proposition: Lemma negate_zero_prod_l x y : -x * y = 0 ↔ x * y = 0.
proof: Proof. split; intros E. apply (injective (-)). now rewrite negate_mult_distr_l, negate_0. apply (injective (-)). now rewrite negate_mult_distr_l, negate_involutive, negate_0. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra