proposition: Lemma pow_negx x n : pow (- x) n = (pow (-1) n) * pow x n.
proof: Proof. have -> : - x = -1 * x by ring. by rewrite Rpow_mult_distr. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval