proposition: Lemma derive_pt_div : forall (f1 f2:R -> R) (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x) (na:f2 x <> 0), derive_pt (f1 / f2) x (derivable_pt_div _ _ _ pr1 pr2 na) = (derive_pt f1 x pr1 * f2 x - derive_pt f2 x pr2 * f1 x) / Rsqr (f2 x).
proof: Proof. intros. assert (H := derivable_derive f1 x pr1). assert (H0 := derivable_derive f2 x pr2). assert (H1 := derivable_derive (f1 / f2)%F x (derivable_pt_div _ _ _ pr1 pr2 na)). elim H; clear H; intros l1 H. elim H0; clear H0; intros l2 H0. elim H1; clear H1; intros l H1. rewrite H; rewrite H0; apply derive_pt_eq_0. assert (H3 := proj2_sig pr1). unfold derive_pt in H; rewrite H in H3. assert (H4 := proj2_sig pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_div; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 Ranalysis2 Lra