proposition: Lemma n_deriv_inc : forall n F H, included (Compact Hab) (Dom (n_deriv_I n F H)).
proof: Proof. intros; simpl in |- *. unfold I, Hab in |- *; apply Derivative_I_n_imp_inc' with n F. apply n_deriv_lemma. Qed.
imports: CoRN.ftc.Differentiability