proposition: Lemma R_infsum_as_IR_convergent : forall (y: R) a, infinit_sum a y -> convergent (fun i : nat => RasIR (a i)).
proof: Proof. unfold infinit_sum. unfold convergent. intros y a conv. assert (cauchy := CV_Cauchy _ (exist _ y conv)). clear conv. unfold Cauchy_crit in cauchy. unfold Cauchy_prop. intros e e0. pose (new_e0 := R_lt_as_IR_back _ _ e0). rewrite -> IR_Zero_as_R in new_e0. assert (sig (fun N => forall n m : nat, (n >= N)%nat -> (m >= N)%nat -> R_dist (sum_f_R0 a n) (sum_f_R0 a m) < IRasR e )). apply constructive_indefinite_description_nat. intros N. apply forall_dec. intros n0. apply forall_dec. intros n1. apply imp_dec. unfold ge. destruct (le_gt_dec N n0). left; auto with *. right; auto with *. apply imp_dec. destruct (le_gt_dec N n1). left; auto with *. right; auto with *. apply Rlt_dec. apply cauchy; auto with *. destruct H as [N HN]. exists (S N). intros m Hm. assert (N <= pred m)%nat by auto with *. assert (HH := HN (pred m) N H (Nat.le_refl N)). clear - HH Hm. destruct m. exfalso. auto with *. rewrite <- R_sum_as_IR. rewrite <- R_sum_as_IR. rewrite <- R_minus_as_IR. apply AbsIR_imp_AbsSmall. stepl (RasIR (Rabs(sum_f_R0 a m - sum_f_R0 a N))); [| now apply R_abs_as_IR]. apply less_leEq. unfold R_dist in HH. stepr (RasIR (IRasR e)); [| now 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)