proposition: Lemma ex_derive_powerRZS (n : Z) (x : R): ((1 <= n)%Z \/ x <> 0) -> ex_derive (fun x : R => powerRZ x (n+1)) x.
proof: Proof. move => H. apply: ex_derive_powerRZ. case: H => [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