proposition: Lemma upper_CRapproximation (x: CR) (e: Qpos): x <= ' (approximate x e + proj1_sig e)%Q.
proof: Proof. intros. rewrite <- CRplus_Qplus. apply CRplus_le_r with (-'proj1_sig e)%CR. assert (' approximate x e + 'proj1_sig e - 'proj1_sig e == ' approximate x e)%CR as E by ring. rewrite E. apply (in_CRball (proj1_sig e) x ('approximate x e)), ball_approx_r. 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