proposition: Lemma conv_fun_series_inv : fun_series_convergent _ _ Hab (fun n => {--} (f n)).
proof: Proof. elim convF; intros contF convF'. exists (fun n : nat => Continuous_I_inv _ _ _ _ (contF n)). cut (forall n : nat, Continuous_I Hab {--} (fun_seq_part_sum f n)). intro H. apply Cauchy_fun_seq_wd with (f := fun n : nat => {--} (fun_seq_part_sum f n)) (contf := H). 2: apply fun_Cauchy_prop_inv with (fun_seq_part_sum_cont _ _ _ _ contF). intro; FEQ. apply contin_imp_inc; Contin. simpl in |- *; unfold seq_part_sum in |- *. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply inv_Sum0. apply Sum0_wd; intro; rational. assumption. Contin. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series