proposition: Lemma CRle_Q : forall (x : CR) (q : Q), ('q <= x)%CR <-> (forall e:Qpos, q <= approximate x e + proj1_sig e)%Q.
proof: Proof. split. - intros. unfold CRle in H. rewrite CRopp_Qopp, CRplus_comm, CRplus_translate in H. specialize (H e). simpl in H. apply (Qplus_le_l _ _ (`e + q)) in H. ring_simplify in H. rewrite Qplus_comm. exact H. - intros. unfold CRle. rewrite CRopp_Qopp, CRplus_comm, CRplus_translate. intro e. simpl. apply (Qplus_le_l _ _ (`e + q)). ring_simplify. rewrite Qplus_comm. apply H. 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