proposition: Lemma Diffble_I_wd : Feq (Compact Hab) F H -> Diffble_I Hab' H.
proof: Proof. intro H0. exists (ProjT1 diffF). eapply Derivative_I_wdl. apply H0. apply projT2. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps