proposition: Lemma ex_derive_powerRZ (n : Z) (x : R): ((0 <= n)%Z \/ x <> 0) -> ex_derive (fun x : R => powerRZ x n) x.
proof: Proof. move => H. apply: (ex_derive_is_derive ((fun x : R => powerRZ x (n)))). exact: is_derive_powerRZ. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval