proposition: Lemma CRisCRing : is_CRing CRasCAbGroup 1%CR CRmultasBinOp.
proof: Proof. apply Build_is_CRing with CRmultAssoc. split. intros x. change (x*1==x)%CR. rewrite <- CR_eq_as_Cauchy_IR_eq. stepl ((CRasCauchy_IR x)[*](CRasCauchy_IR (inject_Q_CR 1))); [| now apply CR_mult_as_Cauchy_IR_mult]. stepl ((CRasCauchy_IR x)[*][1]). rational. apply bin_op_is_wd_un_op_rht; apply: CR_inject_Q_as_Cauchy_IR_inject_Q. intros x. change ((inject_Q_CR 1%Q)*x==x)%CR. rewrite <- CR_eq_as_Cauchy_IR_eq. stepl ((CRasCauchy_IR (inject_Q_CR 1))[*](CRasCauchy_IR x)); [| now apply CR_mult_as_Cauchy_IR_mult]. stepl ([1][*](CRasCauchy_IR x)); [| now apply bin_op_is_wd_un_op_lft; apply: CR_inject_Q_as_Cauchy_IR_inject_Q]. rational. 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_mult_as_Cauchy_IR_mult]. stepr ((CRasCauchy_IR y)[*](CRasCauchy_IR x)); [| now apply CR_mult_as_Cauchy_IR_mult]. rational. intros x y z. change (x*(y+z)==x*y+x*z)%CR. rewrite <- CR_eq_as_Cauchy_IR_eq. stepl ((CRasCauchy_IR x)[*](CRasCauchy_IR (y+z)%CR)); [| now apply CR_mult_as_Cauchy_IR_mult]. stepl ((CRasCauchy_IR x)[*]((CRasCauchy_IR y)[+](CRasCauchy_IR z))); [| now apply bin_op_is_wd_un_op_rht; apply CR_plus_as_Cauchy_IR_plus]. stepr ((CRasCauchy_IR (x*y)%CR)[+](CRasCauchy_IR (x*z)%CR)); [| now apply CR_plus_as_Cauchy_IR_plus]. stepr (((CRasCauchy_IR x)[*](CRasCauchy_IR y))[+]((CRasCauchy_IR x)[*](CRasCauchy_IR z))). apply dist. apply cs_bin_op_wd; apply CR_mult_as_Cauchy_IR_mult. change (CRapartT 1 0)%CR. apply CR_ap_as_Cauchy_IR_ap_2. eapply ap_wd. apply one_ap_zero. apply: CR_inject_Q_as_Cauchy_IR_inject_Q. apply: CR_inject_Q_as_Cauchy_IR_inject_Q. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRFieldOps CoRN.model.abgroups.CRabgroup CoRN.algebra.CRings CoRN.reals.fast.CRcorrect CoRN.tactics.Rational CoRN.tactics.CornTac