proposition: Lemma CRisCGroup : is_CGroup CRasCMonoid CRoppasUnOp.
proof: Proof. split. change (x-x==0)%CR. rewrite <- CR_eq_as_Cauchy_IR_eq. stepl ((CRasCauchy_IR x)[+](CRasCauchy_IR (- x)%CR)); [| now apply CR_plus_as_Cauchy_IR_plus]. stepl ((CRasCauchy_IR x)[+][--](CRasCauchy_IR x)); [| now apply plus_resp_eq; apply CR_opp_as_Cauchy_IR_opp]. apply: eq_transitive. 1:apply cg_rht_inv_unfolded. apply: CR_inject_Q_as_Cauchy_IR_inject_Q. change (-x + x==0)%CR. rewrite <- CR_eq_as_Cauchy_IR_eq. stepl ((CRasCauchy_IR (-x)%CR)[+](CRasCauchy_IR x)); [| now apply CR_plus_as_Cauchy_IR_plus]. stepl ([--](CRasCauchy_IR x)[+](CRasCauchy_IR x)); [| now apply bin_op_is_wd_un_op_lft; apply CR_opp_as_Cauchy_IR_opp]. eapply eq_transitive. apply cg_lft_inv_unfolded. apply: CR_inject_Q_as_Cauchy_IR_inject_Q. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRGroupOps CoRN.model.monoids.CRmonoid CoRN.reals.fast.CRcorrect CoRN.tactics.CornTac