proposition: Lemma CRisCSemiGroup : is_CSemiGroup _ CRplusasBinOp.
proof: Proof. intros x y z. change (x + (y+z)==(x+y)+z)%CR. rewrite <- CR_eq_as_Cauchy_IR_eq. stepl ((CRasCauchy_IR x)[+](CRasCauchy_IR (y+z)%CR)); [| now apply CR_plus_as_Cauchy_IR_plus]. stepl ((CRasCauchy_IR x)[+]((CRasCauchy_IR y)[+](CRasCauchy_IR z))); [| now apply plus_resp_eq; apply CR_plus_as_Cauchy_IR_plus]. stepr ((CRasCauchy_IR (x+y)%CR)[+](CRasCauchy_IR z)); [| now apply CR_plus_as_Cauchy_IR_plus]. stepr (((CRasCauchy_IR x)[+](CRasCauchy_IR y))[+](CRasCauchy_IR z)); [| now apply bin_op_is_wd_un_op_lft; apply CR_plus_as_Cauchy_IR_plus]. apply plus_assoc_unfolded. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRGroupOps CoRN.model.setoids.CRsetoid CoRN.algebra.CGroups CoRN.reals.fast.CRcorrect CoRN.tactics.CornTac