proposition: Lemma Diffble_I_n_imp_inc : forall n F, Diffble_I_n Hab' n F -> included (Compact Hab) (Dom F).
proof: Proof. intros n F H; induction n as [| n Hrecn]. simpl in H; Included. apply Hrecn. exact (le_imp_Diffble_I _ _ (Nat.le_succ_diag_r n) _ H). Qed.
imports: CoRN.ftc.Differentiability