proposition: Lemma derive_pt_Rball_div: forall f g c r x prf prg prfg, Rball c r x -> g x <> 0 -> derive_pt_in (Rball c r) (f / g)%F x prfg = (derive_pt_in (Rball c r) f x prf * g x - f x * derive_pt_in (Rball c r) g x prg) / (g x) ^ 2.
proof: Proof. intros f g c r x [] [] [] x_in gx_neq ; eapply derivable_pt_lim_Rball_uniqueness, derivable_pt_lim_in_div ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics