proposition: Lemma Continuous_I_Sum : forall f : nat -> PartIR, (forall n, Continuous_I Hab (f n)) -> forall m n, Continuous_I Hab (FSum m n f).
proof: Proof. intros. eapply Continuous_I_wd. apply Feq_symmetric; apply FSum_FSum0'. intro; apply contin_imp_inc; auto. apply Continuous_I_minus; apply Continuous_I_Sum0; auto. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac