proposition: Lemma Diffble_I_poly : forall p, Diffble_I Hab' (FPoly _ p).
proof: Proof. intros p. exists (@IntPartIR (FPoly _ (_D_ p)) _ _ Hab (included_IR _)). apply Derivative_I_wdr with (FPoly _ (_D_ p)). apply int_part_int. Deriv. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps