proposition: Lemma filterlim_pow_m_even n : ~~ odd n.+1 -> filterlim (fun x => pow x n.+1) (Rbar_locally m_infty) (Rbar_locally p_infty).
proof: Proof. move => Hodd. rewrite -(odd_double_half n.+1). rewrite -[odd n.+1]Bool.negb_involutive Hodd /= add0n. rewrite -mul2n. apply: filterlim_ext. move => y; by rewrite pow_mult. apply: (filterlim_comp _ _ _ (fun x => x ^ 2) (fun x => x ^ (uphalf n))). apply: filterlim_sqr_m_infty. case: n Hodd => [|n] // Hodd. exact: filterlim_pow_infty. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval