proposition: Lemma Continuous_I_Sum0 : forall f : nat -> PartIR, (forall n, Continuous_I Hab (f n)) -> forall n, Continuous_I Hab (FSum0 n f).
proof: Proof. intros. induction n as [| n Hrecn]. eapply Continuous_I_wd. apply FSum0_0. 2: apply Continuous_I_const. intro; apply contin_imp_inc; auto. eapply Continuous_I_wd. apply FSum0_S. intro; apply contin_imp_inc; auto. apply Continuous_I_plus; auto. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac