proposition: Lemma exp_bound_exp : forall (z:Z) (x:CR), (x <= 'z -> exp_bounded z x == exp x)%CR.
proof: Proof. intros z x H. unfold exp. set (a:=(approximate x (Qpos2QposInf (1 # 1)) + 1)). rewrite <- (CRasIRasCR_id x). rewrite <- exp_bounded_correct. rewrite <- exp_bounded_correct. reflexivity. change (CRasIR x [<=] inj_Q IR (Qceiling a:Q)). rewrite -> IR_leEq_as_CR. autorewrite with IRtoCR. rewrite -> CRasIRasCR_id. apply CRle_trans with ('a)%CR. apply exp_bound_lemma. rewrite -> CRle_Qle. auto with *. change (CRasIR x [<=] inj_Q IR (z:Q)). rewrite -> IR_leEq_as_CR. autorewrite with IRtoCR. rewrite -> CRasIRasCR_id. assumption. 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