proposition: Lemma is_derive_Rpower {x y} (Hx : 0 < x) (Hy : 0 <= y) : is_derive (fun t => Rpower t y) x (y * Rpower x (y - 1)).
proof: Proof. move: (is_derive_n_Rpower 1 y x Hx) => /=. by rewrite big_ord_recl big_ord0 /= Rminus_0_r Rmult_1_r. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval