proposition: Lemma filterlim_pow_infty n : filterlim (pow^~ n.+1) (Rbar_locally p_infty) (Rbar_locally p_infty).
proof: Proof. elim: n => [|n Hn]. apply: (filterlim_ext (fun x => x)). by move => x; rewrite pow_1. exact: filterlim_id. apply: (filterlim_ext (fun x => x * (pow x n.+1))). by move => x. apply: filterlim_comp_2; first exact: filterlim_id. exact: Hn. exact: filterlim_Rbar_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