proposition: Lemma N_Deriv_lemma : forall n F H, Derivative_n n I pI F (N_Deriv n F H).
proof: Proof. intros. elim H; intros incF diffF. split; auto. split; Included. intros a b Hab H0. cut (Diffble_I_n Hab n F). intro H1. 2: auto. eapply Derivative_I_n_wdr. apply Feq_symmetric; apply (N_Deriv_Feq n F (incF, diffF) _ _ Hab H1 H0). apply n_deriv_lemma. Qed.
imports: CoRN.ftc.MoreIntervals