proposition: Lemma Continuous_Sum : forall m n : nat, Continuous I (FSum m n f).
proof: Proof. intros. eapply Continuous_wd. apply Feq_symmetric; apply FSum_FSum0'; Included. apply Continuous_minus; apply Continuous_Sum0. Qed.
imports: CoRN.ftc.MoreIntervals