x y : -x * y = 0 <-> x * y = 0. Proof. split; intros E. - apply (injective (-)). rewrite negate_mult_distr_l, negate_0. trivial. - apply (injective (-)). rewrite negate_mult_distr_l, negate_involutive, negate_0. trivial. Qed.
Require Import Require Import