proposition: Lemma R_infsum_as_IR : forall (y: R) a, Rfunctions.infinit_sum a y -> forall prf, RasIR y [=] series_sum (fun i : nat => RasIR (a i)) prf.
proof: Proof. intros y a Hay prf. unfold series_sum. unfold infinit_sum in *. apply Limits_unique. unfold Cauchy_Lim_prop2. simpl. clear prf. intros e He. assert (sig (fun N => forall n : nat, (n >= N)%nat -> R_dist (sum_f_R0 a n) y < IRasR e )). apply constructive_indefinite_description_nat. intros N. apply forall_dec. intros n0. apply imp_dec. unfold ge. destruct (le_gt_dec N n0). left; auto with *. right; auto with *. apply Rlt_dec. apply (Hay). unfold Rgt. apply R_lt_as_IR. stepl ([0]:IR); [| now symmetry;apply R_Zero_as_IR]. stepr (e); [| now symmetry; apply IRasRasIR_id]. assumption. destruct H as [N HN]. exists (S N). intros m Hm. assert (N <= pred m)%nat. auto with *. assert (HH := HN (pred m) H). clear - HH Hm. destruct m. exfalso. auto with *. rewrite <- R_sum_as_IR. rewrite <- R_minus_as_IR. apply AbsIR_imp_AbsSmall. unfold R_dist in HH. simpl in HH. apply less_leEq. stepl (RasIR (Rabs(sum_f_R0 a m - y))); [| apply R_abs_as_IR]. stepr (RasIR (IRasR e)); [| apply IRasRasIR_id]. apply IR_lt_as_R. assumption. 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)