proposition: Lemma Derivative_I_div : Derivative_I Hab' (F{/}G) ((F'{*}G{-}F{*}G') {/}G{*}G).
proof: Proof. cut (Derivative_I Hab' (F{/}G) (F{*}{--} (G'{/}G{*}G) {+}F'{*}{1/}G)). intro H. eapply Derivative_I_wdr. 2: apply H. apply eq_imp_Feq. Included. apply included_FDiv. Included. Included. intros; apply bnd_imp_ap_zero with I; unfold I in |- *; Included. intros; simpl in |- *; rational. apply Derivative_I_wdl with (F{*}{1/}G). FEQ. Deriv. Qed.
imports: CoRN.ftc.Derivative