proposition: Lemma filterlim_sqrt_p : filterlim sqrt (Rbar_locally' p_infty) (Rbar_locally p_infty).
proof: Proof. apply is_lim_spec. move => M. exists ((Rmax 0 M)²) => x Hx. apply Rle_lt_trans with (1 := Rmax_r 0 M). rewrite -(sqrt_Rsqr (Rmax 0 M)). apply sqrt_lt_1_alt. split. apply Rle_0_sqr. by apply Hx. apply Rmax_l. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis