proposition: Lemma insert_series_conv : fun_series_convergent_IR J insert_series.
proof: Proof. intros a b Hab Hinc. elim (convF _ _ _ Hinc); intros Hcont HCauchy. exists (fun n => included_imp_Continuous _ _ (insert_series_cont n) _ _ _ Hinc). intros e H. elim (HCauchy e H); intros N HN. exists (S N); do 4 intro. cut (m = S (pred m)); [ intro | symmetry; apply Nat.lt_succ_pred with 0; apply Nat.lt_le_trans with (S N); auto with arith ]. cut (n = S (pred n)); [ intro | symmetry; apply Nat.lt_succ_pred with 0; apply Nat.lt_le_trans with (S N); auto with arith ]. generalize H0 H1; clear H1 H0. rewrite H2; rewrite H3; clear H2 H3. intros. cut (N <= pred m); [ intro | auto with arith ]. cut (N <= pred n); [ intro | auto with arith ]. eapply leEq_wdl. apply (HN _ _ H2 H3 x Hx). apply AbsIR_wd. apply cg_minus_wd; apply insert_series_sum_char. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions