proposition: Lemma Diffble_I_nth : forall n : nat, Diffble_I Hab' (F{^}n).
proof: Proof. intro. induction n as [| n Hrecn]. eapply Diffble_I_wd. 2: apply FNth_zero'; Included. apply Diffble_I_const. eapply Diffble_I_wd. 2: apply FNth_mult'; Included. apply Diffble_I_mult; assumption. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps