proposition: Lemma is_LimSup_seq_ext_loc (u v : nat -> R) (l : Rbar) : eventually (fun n => u n = v n) -> is_LimSup_seq u l -> is_LimSup_seq v l.
proof: Proof. case: l => [l | | ] /= [Next Hext] Hu. move => eps. case: (Hu eps) => {Hu} H1 H2 ; split. move => N. case: (H1 (N + Next)%nat) => {H1} n [Hn H1]. exists n ; rewrite -Hext ; intuition. case: H2 => N H2. exists (N + Next)%nat => n Hn. rewrite -Hext ; intuition. move => M N. case: (Hu M (N + Next)%nat) => {Hu} n [Hn Hu]. exists n ; rewrite -Hext ; intuition. move => M. case: (Hu M) => {Hu} N Hu. exists (N + Next)%nat => n Hn. rewrite -Hext ; intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy