proposition: Lemma Derivative_Sum0 : forall n, Derivative I pI (FSum0 n f) (FSum0 n f').
proof: Proof. intros. induction n as [| n Hrecn]. eapply Derivative_wdl. apply FSum0_0; Included. eapply Derivative_wdr. apply FSum0_0; Included. apply Derivative_const. eapply Derivative_wdl. apply FSum0_S; Included. eapply Derivative_wdr. apply FSum0_S; Included. apply Derivative_plus; auto. Qed.
imports: CoRN.ftc.MoreIntervals