proposition: Lemma Diffble_I_imp_le : forall n, 0 < n -> forall F F', Diffble_I_n Hab' n F -> Derivative_I Hab' F F' -> Diffble_I_n Hab' (pred n) F'.
proof: Proof. simple destruct n. intros; exfalso; inversion H. clear n; intros n H F F' H0 H1. elim H0; intros f'' Hf''. simpl in |- *. eapply Diffble_I_n_wd. 2: apply Hf''. apply Derivative_I_unique with F. apply projT2. assumption. Qed.
imports: CoRN.ftc.Differentiability