proposition: Lemma deriv_imp_Diffble_I : forall F F', Derivative_I Hab' F F' -> Diffble_I Hab' F.
proof: Proof. intros F F' H. exists (IntPartIR (derivative_imp_inc' _ _ _ _ _ H)). apply Derivative_I_wdr with F'. apply int_part_int. assumption. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps