proposition: Lemma derive_pt_Rball_inv: forall f c r x pr pr', Rball c r x -> f x <> 0 -> derive_pt_in (Rball c r) (/ f)%F x pr = (- derive_pt_in (Rball c r) f x pr') / (f x) ^ 2.
proof: Proof. intros f c r x [] [] x_in fx_neq ; eapply derivable_pt_lim_Rball_uniqueness, derivable_pt_lim_in_inv ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics