proposition: Lemma is_lim_Rpower y (Hy : 0 < y) : is_lim (fun x => Rpower x y) p_infty p_infty.
proof: Proof. rewrite /Rpower. apply: is_lim_comp => // . exact: is_lim_exp_p. apply: (is_lim_ext (fun x => scal y (ln x))). by move => x0. have {2}-> : p_infty = Rbar_mult y p_infty. by rewrite Rbar_mult_p_l. apply (is_lim_scal_l ln y p_infty p_infty). exact: is_lim_ln_p. exists 0 => x0 Hx0 //. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval