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