proposition: Lemma x_alpha_0 alpha (Halpha : (alpha < -1)%Z) : is_lim (powerRZ^~ (alpha + 1)%Z) p_infty (0%R).
proof: Proof. apply: is_lim_powerRZ_0. by lia. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval