proposition: Lemma derivable_pt_div : forall (f1 f2:R -> R) (x:R), derivable_pt f1 x -> derivable_pt f2 x -> f2 x <> 0 -> derivable_pt (f1 / f2) x.
proof: Proof. unfold derivable_pt. intros f1 f2 x X X0 H. elim X; intros. elim X0; intros. exists ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)). apply derivable_pt_lim_div; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 Ranalysis2 Lra