x y : x * -y = 0 <-> x * y = 0. Proof. etransitivity. 2: apply negate_zero_prod_l. split. - intros E. lhs_V nrapply negate_mult_distr_l. lhs nrapply negate_mult_distr_r. exact E. - intros E. lhs_V nrapply negate_mult_distr_r. lhs nrapply negate_mult_distr_l. exact E. Defined.
Require Import Require Import