proposition: Lemma deriv_n_imp_Diffble_I_n : forall n F F', Derivative_I_n Hab' n F F' -> Diffble_I_n Hab' n F.
proof: Proof. intro; induction n as [| n Hrecn]; intros F F' H. simpl in |- *; simpl in H. elim H; intros. elim b0; auto. simpl in |- *. elim H; intros f' H0 H1. cut (Diffble_I Hab' F); [ intro H2 | exists f'; assumption ]. exists H2. apply Hrecn with F'. eapply Derivative_I_n_wdl. 2: apply H1. apply Derivative_I_unique with F. assumption. apply projT2. Qed.
imports: CoRN.ftc.Differentiability