proposition: Lemma Diffble_I_Sum : forall (f : nat -> PartIR), (forall n, Diffble_I Hab' (f n)) -> forall m n, Diffble_I Hab' (FSum m n f).
proof: Proof. intros. eapply Diffble_I_wd. 2: apply Feq_symmetric; apply FSum_FSum0'; Included. apply Diffble_I_minus; apply Diffble_I_Sum0; auto. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps