proposition: Lemma inject_Q_CR_plus : forall q r : Q, (fun x y : CR => (fun x0 y0 : CR => (y0 < x0)%CR -> False) y x /\ (fun x0 y0 : CR => (y0 < x0)%CR -> False) x y) (' (q + r)%Q)%CR (CRplus (' q)%CR (' r)%CR).
proof: Proof. intros q r. apply CReq_nlt, (CRplus_Qplus q r). Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon