proposition: Lemma Qlt_from_CRlt (a b: Q): (' a < ' b)%CR -> (a < b)%Q.
proof: Proof. Proof with auto. unfold CRltT. unfold CRpos. intros [[e p] H]. revert H. simpl. rewrite CRminus_Qminus. rewrite CRle_Qle. intros. apply Qlt_le_trans with (a + e)%Q. rewrite <-(Qplus_0_r a) at 1. apply Qplus_lt_r... apply Q.Qplus_le_l with (-a)%Q. ring_simplify. rewrite Qplus_comm... 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