proposition: Lemma is_lim_seq_Rbar_loc_seq (x : Rbar) : is_lim_seq (Rbar_loc_seq x) x.
proof: Proof. intros P HP. apply filterlim_Rbar_loc_seq. now apply Rbar_locally'_le. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy