proposition: Lemma is_derive_n_sqrt n x : 0 < x -> is_derive_n sqrt 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. exact Rpower_sqrt. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp