proposition: Lemma R_exp_as_IR : forall x, RasIR (exp x) [=] Exp (RasIR x).
proof: Proof. unfold exp. unfold projT1. intro x; case (exist_exp x). unfold exp_in. intros y rsums. rewrite -> ( R_infsum_f_as_IR x y ((fun x i => / INR (fact i) * Rpow_def.pow x i)) rsums (R_infsum_as_IR_convergent _ _ rsums) ). simpl. apply series_sum_wd. intro i. autorewrite with RtoIR. replace (/ nring (fact i)) with (1 / nring (fact i)). 2: field; apply (nring_fac_ap_zero RReals i). cut (Dom (f_rcpcl' IR) (RasIR (nring (R:=RRing) (fact i)))). intro Hy. rewrite -> (R_recip_as_IR (nring (fact i)) Hy). clear. rewrite -> (cg_inv_zero IR (RasIR x)). apply mult_wdl. apply div_wd. reflexivity. apply (R_nring_as_IR (fact i)). simpl. stepl (nring (R:=IR) (fact i)). apply (nring_fac_ap_zero IR i). symmetry. apply (R_nring_as_IR). Qed.
imports: Coq.QArith.QArith Coq.QArith.Qreals Coq.QArith.QArith_base CoRN.tactics.CornTac Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun CoRN.coq_reals.Rreals CoRN.reals.iso_CReals CoRN.reals.CauchySeq Coq.Reals.Rtrigo_def CoRN.transc.PowerSeries Coq.Logic.ConstructiveEpsilon Coq.Reals.Rlogic Coq.Reals.Reals CoRN.transc.Pi CoRN.transc.MoreArcTan CoRN.logic.PropDecid CoRN.transc.Exponential Coq(Lia Lra)