proposition: Lemma CRbound_distance_from_below : forall (x : CR) (q : Q) (a b : Qpos), (approximate x a <= q)%Q -> ('q <= x)%CR -> (Qabs (approximate x b - q) <= `a + `b)%Q.
proof: Proof. intros. assert (x <= 'q + '`a)%CR. { apply (CRle_trans (upper_CRapproximation x a)). rewrite CRplus_Qplus. apply CRle_Qle. apply Qplus_le_l. exact H. } apply Qabs_case. - intros. pose proof (lower_CRapproximation x b). apply (Qplus_le_l _ _ (q-`b)). ring_simplify. setoid_replace (-(1#1)*`b)%Q with (- ` b)%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply CRle_Qle. apply (CRle_trans H3). rewrite <- CRplus_Qplus. exact H1. - intros. pose proof (upper_CRapproximation x b). apply (Qplus_le_r _ _ (approximate x b)). ring_simplify. rewrite (Qplus_comm (approximate x b)), <- Qplus_assoc. apply (Qle_trans _ (0 + (approximate x b + `b))). rewrite Qplus_0_l. apply CRle_Qle. apply (CRle_trans H0), H3. apply Qplus_le_l. apply Qpos_nonneg. 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