proposition: Lemma deriv_n_imp_diffble : forall n : nat, 0 < n -> forall F F' : PartIR, Derivative_I_n Hab' n F F' -> Diffble_I Hab' F.
proof: Proof. simple destruct n. intros; exfalso; inversion H. clear n; intros n H F F' H0. elim H0; clear H0; intros f'' H0 H1. exists f''; assumption. Qed.
imports: CoRN.ftc.Differentiability