proposition: Lemma is_derive_n_powerRZ m n x : (0 <= m)%Z \/ x <> 0 -> is_derive_n (powerRZ^~ m) n x (match m with | Z0 => if n is O then 1%R else 0%R | Z.pos p => \big[Rmult/1%R]_(i < n) INR (Pos.to_nat p - i) * x ^ (Pos.to_nat p - n) | Z.neg p => \big[Rmult/1%R]_(i < n) - INR (Pos.to_nat p + i) * / x ^ (Pos.to_nat p + n) end).
proof: Proof. move=> Hor. rewrite /powerRZ; case: m Hor => [|p|p] Hor. - case: n => [|n] //; exact: is_derive_n_const. - by apply: is_derive_n_pow; apply/ltP/Pos2Nat.is_pos. - apply: is_derive_n_inv_pow; first exact/ltP/Pos2Nat.is_pos. by case: Hor; first by case. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp