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