proposition: Lemma n_deriv_lemma : forall n F H, Derivative_I_n Hab' n F (n_deriv_I n F H).
proof: Proof. intro; induction n as [| n Hrecn]; intros. simpl in |- *; simpl in H; FEQ. elim H; intros Hf Hf'. exists (ProjT1 Hf). apply projT2. simpl in |- *. cut (Diffble_I_n Hab' n (PartInt (ProjT1 Hf))). intro H0. apply Derivative_I_n_wdr with (n_deriv_I _ _ H0). 2: apply Hrecn. apply n_deriv_I_wd. unfold I, Hab in |- *; apply Derivative_I_unique with F. apply projT2. apply projT2. elim H; intros. eapply Diffble_I_n_wd. 2: apply p. apply Derivative_I_unique with F; apply projT2. Qed.
imports: CoRN.ftc.Differentiability