proposition: Lemma is_lim_seq_p_infty_Reals (u : nat -> R) : is_lim_seq u p_infty <-> cv_infty u.
proof: Proof. split => Hl. move => M. case: (Hl (fun x => M < x)) => {Hl} [ | N Hl]. by exists M. by exists N. move => P [M HP]. eapply filter_imp. by apply HP. case: (Hl M) => {Hl} N HN. by exists N. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy