proposition: Lemma is_RInt_powerRZ (alpha : Z) (a b : R) (HneqN1 : alpha <> (-1)%Z) (H : 0 < a <= b) : is_RInt (powerRZ^~ alpha) a b ((powerRZ b (alpha + 1) - powerRZ a (alpha + 1)) / IZR (alpha + 1)).
proof: Proof. have neq0 : IZR (alpha + 1) <> 0. apply: not_0_IZR. by rewrite Z.add_move_0_r; exact: HneqN1. pose F := fun x => powerRZ x (alpha+1) / IZR (alpha + 1). have -> : ((powerRZ b (alpha + 1) - powerRZ a (alpha + 1)) / IZR (alpha + 1)) = F b - F a. rewrite /F. field => // . have xneq0 : forall x, Rmin a b <= x <= Rmax a b -> x <> 0. move => x [Hax Hxb]. apply: Rgt_not_eq. apply: (Rlt_le_trans 0 (Rmin a b) x) => // . by case: H => [H0a Hab]; rewrite Rmin_left. apply: is_RInt_derive => x Hx. rewrite /F. have -> : (powerRZ x alpha) = ((IZR (alpha+1)) * ((powerRZ x alpha)) / (IZR (alpha+1))). by field. rewrite !/Rdiv. apply: is_derive_scal_l. apply: is_derive_powerRZS. by right; apply xneq0. apply: ex_derive_continuous. apply: (ex_derive_n_powerRZ alpha 1). by right; apply xneq0. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval