proposition: Lemma filterlim_pow_m_odd n : odd n.+1 -> filterlim (fun x => pow x n.+1) (Rbar_locally m_infty) (Rbar_locally m_infty).
proof: Proof. move => Hodd. case: n Hodd => [|n] Hodd. - apply: (filterlim_ext id). by move => x /=; rewrite Rmult_1_r. exact: filterlim_id. apply: (filterlim_ext (fun x => x * pow x n.+1)). by move => x. apply: filterlim_comp_2. exact: filterlim_id. by apply: filterlim_pow_m_even. by apply: 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