proposition: Lemma CR_ring_ext_nlt : ring_eq_ext CRplus CRmult CRopp (fun x y : CR => (fun x0 y0 : CR => (y0 < x0)%CR -> False) y x /\ (fun x0 y0 : CR => (y0 < x0)%CR -> False) x y).
proof: Proof. split. - intros x y H z t H0. apply CReq_nlt. apply CReq_nlt in H. apply CReq_nlt in H0. rewrite H, H0. reflexivity. - intros x y H z t H0. apply CReq_nlt. apply CReq_nlt in H. apply CReq_nlt in H0. rewrite H, H0. reflexivity. - intros x y H. apply CReq_nlt. apply CReq_nlt in H. rewrite H. reflexivity. 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