proposition: Lemma Diffble_Sum : forall f, (forall n, Diffble I pI (f n)) -> forall m n, Diffble I pI (FSum m n f).
proof: Proof. intros f hypF m n. eapply Diffble_wd. apply Feq_symmetric; apply FSum_FSum0'. intro; apply Diffble_imp_inc with pI; auto. apply Diffble_minus; apply Diffble_Sum0; auto. Qed.
imports: CoRN.ftc.MoreIntervals