proposition: Lemma Derivative_div : Derivative I pI (F{/}G) ((F'{*}G{-}F{*}G') {/}G{*}G).
proof: Proof. elim derF; intros incF Hf. elim Hf; intros incF' Hf'. elim derG; intros incG derivG. elim derivG; intros incG' Hg'. clear Hf derivG. cut (forall x : IR, I x -> forall Hx, Part G x Hx [#] [0]); intros. split. Included. split. apply included_FDiv. apply included_FMinus; Included. Included. intros; simpl in |- *; apply mult_resp_ap_zero; auto. Deriv. Included. Qed.
imports: CoRN.ftc.MoreIntervals