proposition: Lemma Derivative_Sum : forall m n, Derivative I pI (FSum m n f) (FSum m n f').
proof: Proof. intros. eapply Derivative_wdl. apply Feq_symmetric; apply FSum_FSum0'; Included. eapply Derivative_wdr. apply Feq_symmetric; apply FSum_FSum0'; Included. apply Derivative_minus; apply Derivative_Sum0. Qed.
imports: CoRN.ftc.MoreIntervals