proposition: Lemma Diffble_I_minus : Diffble_I Hab' (F{-}G).
proof: Proof. apply Diffble_I_wd with (F{+}{--}G). apply Diffble_I_plus. assumption. apply Diffble_I_inv; assumption. FEQ. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps