proposition: Lemma insert_series_sum : Feq J (FSeries_Sum convF) (FSeries_Sum insert_series_conv).
proof: Proof. set (contF := convergent_imp_Continuous _ _ convF) in *. apply FLim_unique_IR with (fun n => FSum0 n f) (fun n => Continuous_Sum0 _ _ contF n) (Continuous_FSeries_Sum _ _ convF) (Continuous_FSeries_Sum _ _ insert_series_conv). apply FSeries_conv. red in |- *; intros. assert (convS := FSeries_conv _ _ insert_series_conv (Continuous_Sum0 _ _ insert_series_cont) (Continuous_FSeries_Sum _ _ insert_series_conv) _ _ _ Hinc). intros e H. elim (convS e H); intros N HN. clear convS; exists N; intros. eapply leEq_wdl. apply (HN (S n) (le_S _ _ H0) _ Hx). apply AbsIR_wd; apply cg_minus_wd. 2: algebra. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. eapply eq_transitive_unfolded. 2: apply (insert_series_sum_char n x (contin_imp_inc _ _ _ _ (included_imp_Continuous _ _ (Continuous_Sum0 _ _ contF n) _ _ _ Hinc) _ Hx) (contin_imp_inc _ _ _ _ (included_imp_Continuous _ _ (Continuous_Sum0 _ _ insert_series_cont (S n)) _ _ _ Hinc) _ Hx)). unfold fun_seq_part_sum in |- *; algebra. unfold fun_seq_part_sum in |- *; algebra. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions