proposition: Lemma is_derive_n_Rpower n a x : 0 < x -> is_derive_n (Rpower^~ a) n x (\big[Rmult/1%R]_(i < n) (a - INR i) * Rpower x (a - INR n)).
proof: Proof. move: a x; elim: n => [|n IHn] a x Hx. rewrite big_ord0. by rewrite /= Rmult_1_l Rminus_0_r. apply is_derive_Sn. apply: locally_open x Hx. apply open_gt. move => /= x Hx. eexists. now apply is_derive_Reals, derivable_pt_lim_power. apply is_derive_n_ext_loc with (fun x => a * Rpower x (a - 1)). 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_power. rewrite big_ord_recl; rewrite [INR ord0]/= Rminus_0_r Rmult_assoc. apply is_derive_n_scal_l. rewrite S_INR. replace (a - (INR n + 1)) with (a - 1 - INR n) by ring. rewrite (eq_bigr (P := xpredT) (fun i2 : 'I_n => a - 1 - INR i2)); last first. move=> [i Hi] _; rewrite plus_INR /=; ring. exact: IHn. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp