proposition: Lemma Qle_CRle_r (x y: CR): (forall y', y <= ' y' -> x <= ' y') <-> x <= y.
proof: Proof. Proof with auto. split; intros. 2: apply CRle_trans with y... apply from_DN. apply (DN_bind (CRle_lt_dec x y)). intros [?|W]. apply DN_return... exfalso. destruct (CRlt_Qmid _ _ W) as [w [A B]]. pose proof (H w (CRlt_le_weak _ _ A)). apply (CRle_not_lt x ('w)%CR)... 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