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