proposition: Lemma N_Deriv_S : forall n F H HS, Derivative I pI (N_Deriv n F H) (N_Deriv (S n) F HS).
proof: Proof. intros n F H H'. split; Included. split; Included. elim H; intros incF diffFn. elim H'; intros incF' diffFSn. intros a b Hab H0. cut (Diffble_I_n Hab n F). intro H1. 2: auto. cut (Diffble_I_n Hab (S n) F). intro H2. 2: auto. eapply Derivative_I_wdl. apply Feq_symmetric; apply (N_Deriv_Feq n F (incF, diffFn) _ _ Hab H1 H0). eapply Derivative_I_wdr. apply Feq_symmetric; apply (N_Deriv_Feq _ _ (incF', diffFSn) _ _ Hab H2 H0). apply n_Sn_deriv. Qed.
imports: CoRN.ftc.MoreIntervals