proposition: Lemma is_lim_pow_infty n : is_lim (fun x => x^n.+1) p_infty p_infty.
proof: Proof. elim: n => [|n Hn]. - apply: (is_lim_ext id) => // . by move => y; rewrite pow_1. - apply: (is_lim_ext (fun x => x * x^n.+1)). by move => y. have {2}-> : p_infty = Rbar_mult p_infty p_infty => // . apply: is_lim_mult => // . Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval