proposition: Lemma Continuous_Sum0 : forall n : nat, Continuous I (FSum0 n f).
proof: Proof. intros. induction n as [| n Hrecn]. eapply Continuous_wd. apply FSum0_0; Included. Contin. eapply Continuous_wd. apply FSum0_S; Included. Contin. Qed.
imports: CoRN.ftc.MoreIntervals