proposition: Lemma CR_ring_nlt : ring_theory 0%CR 1%CR CRplus CRmult (fun x y : CR => CRplus x (- y)%CR) 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. destruct CR_ring_theory. split. - intro x. apply CReq_nlt, Radd_0_l. - intros x y. apply CReq_nlt, Radd_comm. - intros x y z. apply CReq_nlt, Radd_assoc. - intro x. apply CReq_nlt, Rmul_1_l. - intros x y. apply CReq_nlt, Rmul_comm. - intros x y z. apply CReq_nlt, Rmul_assoc. - intros x y z. apply CReq_nlt, Rdistr_l. - intros x y. apply CReq_nlt, Rsub_def. - intro x. apply CReq_nlt, Ropp_def. 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