proposition: Lemma CR_ring_theory : @ring_theory CR 0 1 (ucFun2 CRplus_uc) CRmult (fun (x y:CR) => (x + - y)) CRopp (@msp_eq CR).
proof: Proof. split. - exact CRplus_0_l. - exact CRplus_comm. - exact CRplus_assoc. - exact CRmult_1_l. - exact CRmult_comm. - intros. symmetry. apply CRmult_assoc. - exact CRmult_plus_distr_r. - reflexivity. - intros x e1 e2. simpl. unfold Cap_raw;simpl. rewrite Qplus_0_r. rewrite Qplus_opp_r. apply Qball_Reflexive. apply (Qpos_nonneg (e1+e2)). Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders