proposition: Lemma ring_opp_mul_l : forall x y, -(x * y) == -x * y.
proof: Proof. intros x y;rewrite <- (ring_add_0_l (- x * y)). rewrite ring_add_comm . rewrite <- (ring_opp_def (x*y)). rewrite ring_add_assoc . rewrite <- ring_distr_l. rewrite (ring_add_comm (-x));rewrite ring_opp_def . rewrite ring_mul_0_l;rewrite ring_add_0_l ;reflexivity. Qed.
imports: Setoid BinPos BinNat Morphisms Setoid Bool ZArith_base Algebra_syntax