proposition: Lemma exp_bound_lemma : forall x : CR, (x <= ' (approximate x (Qpos2QposInf (1 # 1)) + 1)%Q)%CR.
proof: Proof. intros x. assert (X:=ball_approx_l x (1#1)). rewrite <- CRAbsSmall_ball in X. destruct X as [X _]. simpl in X. rewrite <- CRplus_Qplus. apply CRle_trans with (doubleSpeed x). rewrite -> (doubleSpeed_Eq x); apply CRle_refl. intros e. assert (Y:=X e). simpl in *. do 2 (unfold Cap_raw in *; simpl in * ). apply (Qle_trans _ _ _ Y). ring_simplify. apply Qle_refl. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.iso_CReals Coq.QArith.Qpower CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.transc.PowerSeries CoRN.reals.fast.CRpower CoRN.transc.Exponential CoRN.transc.RealPowers CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.reals.fast.CRsign CoRN.reals.Q_in_CReals Coq.QArith.Qabs Coq.QArith.Qround CoRN.tactics.CornTac MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra