proposition: Lemma is_derive_inv (f : R -> R) (x l : R) : is_derive f x l -> f x <> 0 -> is_derive (fun y : R => / f y) x (-l/(f x)^2).
proof: Proof. move => Hf Hl. eapply filterdiff_ext_lin. apply filterdiff_ext with (fun y => 1/f y). move => t ; by rewrite /Rdiv Rmult_1_l. apply is_derive_Reals. apply derivable_pt_lim_div. apply derivable_pt_lim_const. apply is_derive_Reals. exact Hf. exact Hl. simpl => y ; apply f_equal. rewrite /= /Rsqr ; by field. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv