proposition: Lemma is_derive_powerRZS (n : Z) (x : R): ((1 <= n)%Z \/ x <> 0) -> is_derive (fun x : R => powerRZ x (n+1)) x (IZR (n+1) * (powerRZ x n)).
proof: Proof. move => Hnx. move: (is_derive_powerRZ (n+1) x). rewrite Z.add_simpl_r // ; apply. case: Hnx => [Hn | Hx]. left; lia. by right. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval