proposition: Lemma exp_bounded_correct : forall (z:Z) x, closer (inj_Q _ (z:Q)) x -> (IRasCR (Exp x)==exp_bounded z (IRasCR x))%CR.
proof: Proof. intros z x Hx. assert (Z:Continuous (closer (inj_Q IR (z:Q))) Expon). apply (Included_imp_Continuous realline). Contin. Included. apply (fun a b c => @ContinuousCorrect _ a Expon Z b c x I); auto with *. constructor. intros q [] H. transitivity (exp_bound_uc z q);[|]. change (' q)%CR with (Cunit_fun _ q). unfold exp_bounded. pose proof (Cbind_correct QPrelengthSpace (exp_bound_uc z)). apply ucEq_equiv in H0. rewrite (H0 (Cunit_fun Q_as_MetricSpace q)). clear H0. apply BindLaw1. change (rational_exp (Qmin z q) == IRasCR (Exp (inj_Q IR q)))%CR. rewrite -> rational_exp_correct. apply IRasCR_wd. apply Exp_wd. apply inj_Q_wd. simpl. rewrite <- Qle_min_r. apply leEq_inj_Q with IR. 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