proposition: Lemma CR_Q_ring_morphism : ring_morph 0%CR 1%CR (ucFun2 CRplus_uc) CRmult (fun x y => (x + - y)) CRopp (@msp_eq CR) (0%Q) (1%Q) Qplus Qmult Qminus Qopp Qeq_bool (inject_Q_CR).
proof: Proof. split; try reflexivity. apply CRplus_Qplus. apply CRminus_Qminus. intros x y; rewrite -> CRmult_Qmult; reflexivity. apply CRopp_Qopp. intros x y H. rewrite -> CReq_Qeq. apply Qeq_bool_eq. assumption. 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