proposition: Lemma Diffble_I_inv : Diffble_I Hab' {--}F.
proof: Proof. elim diffF; intros F' derF. exists (IInv F'). eapply Derivative_I_wdr. apply part_int_inv with (F := PartInt F'). apply Feq_reflexive; Included. Deriv. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps