proposition: Lemma is_derive_powerRZ (n : Z) (x : R): ((0 <= n)%Z \/ x <> 0) -> is_derive (fun x : R => powerRZ x n) x (IZR n * (powerRZ x (n - 1))).
proof: Proof. move => Hnx. move: (is_derive_n_powerRZ n 1 x Hnx). case Hn : n => [|p|p] /= . - by rewrite !Rmult_0_l; move => _; apply: is_derive_const. - rewrite big_ord_recl /= big_ord0 /= subn0 Rmult_1_r. rewrite INR_IZR_INZ positive_nat_Z. rewrite pow_powerRZ. congr (is_derive _ _ (_ * powerRZ _ _)). rewrite -> Nat2Z.inj_sub by now rewrite Nat.le_succ_l; apply Pos2Nat.is_pos. now rewrite positive_nat_Z. - rewrite big_ord_recl /= big_ord0 /= addn0 Rmult_1_r. rewrite INR_IZR_INZ positive_nat_Z. by rewrite Pos2Nat.inj_add. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval