proposition: Lemma CRlt_le_trans (x y z: CR): x < y -> y <= z -> x < z.
proof: Proof. Proof with auto. intros [e ?] ?. exists e. apply CRle_trans with (y - x)%CR... assert (z - x - (y - x) == z - y)%CR as E by ring. unfold CRle. rewrite E... 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