proposition: Lemma Qle_CRle_l (x y: CR): (forall x', ' x' <= x -> ' x' <= y) <-> x <= y.
proof: Proof. Proof with auto. intros. rewrite CRle_opp. rewrite <- Qle_CRle_r. split; intros. rewrite CRle_opp, CRopp_opp, CRopp_Qopp. apply H. rewrite CRle_opp, CRopp_Qopp, Qopp_opp... rewrite CRle_opp, CRopp_Qopp. apply H. rewrite CRle_opp, CRopp_Qopp, CRopp_opp, Qopp_opp... 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