proposition: Lemma Derivative_I_Sum : forall f f' : nat -> PartIR, (forall n, Derivative_I Hab' (f n) (f' n)) -> forall m n, Derivative_I Hab' (FSum m n f) (FSum m n f').
proof: Proof. intros. eapply Derivative_I_wdl. apply Feq_symmetric; apply FSum_FSum0'; Included. eapply Derivative_I_wdr. apply Feq_symmetric; apply FSum_FSum0'; Included. apply Derivative_I_minus; apply Derivative_I_Sum0; auto. Qed.
imports: CoRN.ftc.Derivative