proposition: Lemma filterlim_sqr_m_infty: filterlim (pow^~ 2%N) (Rbar_locally m_infty) (Rbar_locally p_infty).
proof: Proof. apply: (filterlim_ext (fun x => x * x)); first by move => y; rewrite /= ?Rmult_1_r. suff -> : p_infty = Rbar_mult m_infty m_infty => // . apply: filterlim_comp_2; try exact: filterlim_id. 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