proposition: Lemma is_derive_n_pow : forall m, (0 < m)%nat -> forall n x, is_derive_n (fun x => x ^ m)%R n x (\big[Rmult/1%R]_(i < n) INR (m - i) * x ^ (m - n))%R.
proof: Proof. move=> m Hm; help_is_derive_n_whole n x. - move=> x; rewrite big1 /= ?(addn0, subn0, Rmult_1_l) //. by case. - auto_derive =>//. by rewrite big_ord_recl big_ord0 /= subn0 subn1 /= Rmult_1_l Rmult_1_r. - auto_derive =>//. rewrite [in RHS]big_ord_recr /= /Rdiv; rewrite Rmult_assoc; congr Rmult. by rewrite Rmult_1_l !subnS. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp