proposition: Lemma Derivative_n_Sn : forall F n fn fSn, Derivative_n n I pI F fn -> Derivative_n (S n) I pI F fSn -> Derivative I pI fn fSn.
proof: Proof. intros F n fn fSn H H0. cut (Diffble_n n I pI F); [ intro H1 | eapply Derivative_n_imp_Diffble_n; apply H ]. cut (Diffble_n (S n) I pI F); [ intro H2 | eapply Derivative_n_imp_Diffble_n; apply H0 ]. apply Derivative_wdl with (N_Deriv _ _ H1). apply Derivative_n_unique with n F. apply N_Deriv_lemma. auto. apply Derivative_wdr with (N_Deriv _ _ H2). apply Derivative_n_unique with (S n) F. apply N_Deriv_lemma. auto. apply N_Deriv_S. Qed.
imports: CoRN.ftc.MoreIntervals