proposition: Lemma CRle_alt : forall (x y : CR), x <= y <-> forall e:Qpos, (-(2#1)*proj1_sig e <= approximate y e - approximate x e)%Q.
proof: Proof. split. - intros. apply Qnot_lt_le. intro abs. pose proof (lower_CRapproximation x e). pose proof (upper_CRapproximation y e). apply (Qplus_lt_l _ _ (`e + approximate x e)) in abs. ring_simplify in abs. setoid_replace (approximate x e + -(1#1) * `e)%Q with (approximate x e - `e)%Q in abs by (unfold equiv, stdlib_rationals.Q_eq; ring). apply CRlt_Qlt in abs. apply (CRle_lt_trans _ _ _ H1) in abs. clear H1. apply (CRlt_le_trans _ _ _ abs) in H0. apply CRle_not_lt in H. contradiction. exact H0. - intros. intro e. specialize (H ((1#2)*e)%Qpos). simpl in H. setoid_replace (- (2#1) * ((1 # 2) * ` e))%Q with (-`e)%Q in H by (unfold equiv, stdlib_rationals.Q_eq; ring). 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