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