proposition: Lemma Derivative_n_1 : forall F G, Derivative I pI F G -> Derivative_n 1 I pI F G.
proof: Proof. intros F G H. cut (Diffble I pI F). intro H0. apply Derivative_n_wdr with (Deriv _ H0). apply Derivative_unique with pI F. apply Deriv_lemma. auto. unfold Deriv in |- *; apply N_Deriv_lemma. apply Derivative_imp_Diffble with G; auto. Qed.
imports: CoRN.ftc.MoreIntervals