proposition: Lemma int_x_alpha alpha A B (H : 0 < A <= B) (Halpha: alpha <> (-1)%Z) : is_RInt (powerRZ^~ alpha) A B ((powerRZ B (alpha + 1) - powerRZ A (alpha + 1)) / IZR (alpha + 1)).
proof: Proof. apply: is_RInt_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