proposition: Lemma Derivative_I_Sum0 : forall f f' : nat -> PartIR, (forall n, Derivative_I Hab' (f n) (f' n)) -> forall n, Derivative_I Hab' (FSum0 n f) (FSum0 n f').
proof: Proof. intros. induction n as [| n Hrecn]. eapply Derivative_I_wdl. apply FSum0_0; Included. eapply Derivative_I_wdr. apply FSum0_0; Included. apply Derivative_I_const. eapply Derivative_I_wdl. apply FSum0_S; Included. eapply Derivative_I_wdr. apply FSum0_S; Included. apply Derivative_I_plus; auto. Qed.
imports: CoRN.ftc.Derivative