proposition: Lemma is_derive_n_ln n x : 0 < x -> is_derive_n ln n x (match n with | 0 => ln x | n.+1 => (\big[Rmult/1%R]_(i < n) - INR (1 + i) * / x ^ (1 + n))%R end).
proof: Proof. case: n => [|n] Hx; first done. apply is_derive_Sn. apply: locally_open x Hx. apply open_gt. move => /= x Hx. eexists. now apply is_derive_Reals, derivable_pt_lim_ln. have := is_derive_n_inv n x (Rgt_not_eq _ _ Hx). apply: is_derive_n_ext_loc. apply: locally_open x Hx. apply open_gt. move => /= x Hx. apply sym_eq, is_derive_unique. now apply is_derive_Reals, derivable_pt_lim_ln. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp