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