proposition: Lemma ring_opp_mul_r : 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_r . rewrite (ring_add_comm (-y));rewrite ring_opp_def . rewrite ring_mul_0_r;rewrite ring_add_0_l ;reflexivity. Qed.
imports: Setoid BinPos BinNat Morphisms Setoid Bool ZArith_base Algebra_syntax