proposition: Lemma is_lim_sqrt_p (f : R -> R) (x : Rbar) : is_lim f x p_infty -> is_lim (fun x => sqrt (f x)) x p_infty.
proof: Proof. intros. eapply filterlim_comp, filterlim_sqrt_p. by apply H. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis