proposition: Lemma Diffble_I_div : Diffble_I Hab' (F{/}G).
proof: Proof. apply Diffble_I_wd with (F{*}{1/}G). apply Diffble_I_mult. assumption. apply Diffble_I_recip; assumption. FEQ. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps