proposition: Lemma derivable_pt_lim_in_inv: forall (D : R -> Prop) f x l, D x -> f x <> 0 -> derivable_pt_lim_in D f x l -> derivable_pt_lim_in D (/ f)%F x (- l / (f x ^ 2)).
proof: Proof. intros D f x l Dx Hneq Hf ; assert (f_cont: continuity_pt_in D f x) by (eapply derivable_pt_in_continuity_pt_in ; eexists ; eassumption). destruct (continuity_not_eq_Rball _ _ _ 0 Dx f_cont Hneq) as [alp [alp_pos Halp]] ; eapply limit1_in_ext_strong. eassumption. intros y y_bd [y_in y_neq] ; symmetry ; eapply growth_rate_inv_decomp ; try assumption. apply Halp ; assumption. replace (- l / f x ^ 2) with (- (l / f x ^ 2)) by (unfold Rdiv ; ring). apply limit_Ropp ; unfold Rdiv ; apply limit_mul ; [apply Hf |]. apply limit_inv ; [| apply pow_nonzero ; assumption]. apply limit_mul ; [apply limit_free | rewrite Rmult_1_r] ; eapply limit1_imp, f_cont. intros y [y_in y_neq] ; assumption. assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics