proposition: Lemma is_lim_sqr_infty: is_lim (pow^~ 2%N) m_infty p_infty.
proof: Proof. apply: (is_lim_ext (fun x => x * x)); first by move => y; rewrite /= ?Rmult_1_r. suff -> : p_infty = Rbar_mult m_infty m_infty => // . by 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