proposition: Lemma is_LimInf_seq_ext_loc (u v : nat -> R) (l : Rbar) : eventually (fun n => u n = v n) -> is_LimInf_seq u l -> is_LimInf_seq v l.
proof: Proof. case => N Hext Hu. apply is_LimSup_opp_LimInf_seq. apply is_LimSup_seq_ext_loc with (fun n => - u n). exists N => n Hn ; by rewrite Hext. by apply is_LimSup_opp_LimInf_seq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy