proposition: Lemma derive_Rball_div: forall f g c r x prf prg prfg, g x <> 0 -> derive_Rball c r (f / g)%F prfg x = (derive_Rball c r f prf x * g x - f x * derive_Rball c r g prg x) / (g x) ^ 2.
proof: Proof. intros ; unfold derive_Rball ; destruct (in_Rball_dec c r x) as [x_in | x_nin] ; [apply derive_pt_Rball_div ; assumption | rewrite Rmult_0_r, Rmult_0_l, Rminus_0_r, Rdiv_0_l ; reflexivity]. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics