proposition: Lemma CRisCAbGroup : is_CAbGroup CRasCGroup.
proof: Proof. intros x y. change (x+y==y+x)%CR. rewrite <- CR_eq_as_Cauchy_IR_eq. stepl ((CRasCauchy_IR x)[+](CRasCauchy_IR y)); [| now apply CR_plus_as_Cauchy_IR_plus]. stepr ((CRasCauchy_IR y)[+](CRasCauchy_IR x)); [| now apply CR_plus_as_Cauchy_IR_plus]. apply cag_commutes. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.groups.CRgroup CoRN.reals.fast.CRcorrect CoRN.algebra.CAbGroups CoRN.tactics.CornTac