proposition: Lemma is_lim_seq_le_p_loc (u v : nat -> R) : eventually (fun n => u n <= v n) -> is_lim_seq u p_infty -> is_lim_seq v p_infty.
proof: Proof. apply filterlim_ge_p_infty. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy