proposition: Lemma cam_commutes_unfolded : forall x y : M, x[+]y [=] y[+]x.
proof: Proof. Proof cam_commutes. End AbMonoid_Axioms. Global Instance cm_Sum_AbMonoid_Proper: forall {M: CAbMonoid}, Proper (SetoidPermutation (@st_eq M) ==> @st_eq M) cm_Sum. Proof. repeat intro. apply cm_Sum_Proper. apply cam_proof. assumption. Qed.
imports: CoRN.algebra.CMonoids CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms