proposition: Theorem Xderive_pt_inv : forall f f' x, Xderive_pt f x f' -> Xderive_pt (fun x => Xinv (f x)) x (Xneg (Xdiv f' (Xsqr (f x)))).
proof: Proof. intros f f' x Hf. xtotal. elim Y. apply Rmult_0_l. intro v. apply derivable_pt_lim_eq_locally with (inv_fct (proj_fun v f)). apply locally_true_imp with (2 := derivable_imp_defined_ne _ _ _ _ _ X Y0 Hf). intros x (w, (Hw1, Hw2)). unfold inv_fct, proj_fun. rewrite Hw2. destruct (is_zero_spec w). now elim Hw1. apply refl_equal. apply derivable_pt_lim_eq with (div_fct (fct_cte 1) (proj_fun v f)). intro x. unfold div_fct, fct_cte, Rdiv. apply Rmult_1_l. replace (- (r0 / Rsqr r1))%R with ((0 * proj_fun v f r - r0 * fct_cte 1 r) / Rsqr (proj_fun v f r))%R. apply (derivable_pt_lim_div (fct_cte 1)). apply derivable_pt_lim_const. apply Hf. unfold proj_fun. now rewrite X. unfold proj_fun, fct_cte. rewrite X. now field. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal