proposition: Lemma is_derive_n_invsqrt n x : 0 < x -> is_derive_n (fun t => / sqrt t) n x (\big[Rmult/1%R]_(i < n) (-/2 - INR i) * Rpower x (-/2 - INR n)).
proof: Proof. move=> Hx. have := is_derive_n_Rpower n (-/2) x Hx. apply: is_derive_n_ext_loc. apply: locally_open x Hx. apply open_gt. by move=> x Hx; rewrite Rpower_Ropp Rpower_sqrt. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp