proposition: Lemma is_sup_seq_ext (u v : nat -> Rbar) (l : Rbar) : (forall n, u n = v n) -> is_sup_seq u l -> is_sup_seq v l.
proof: Proof. case: l => [l | | ] Heq ; rewrite /is_sup_seq => Hu. move => eps ; case: (Hu eps) => {Hu} Hu1 Hu2 ; split. move => n ; by rewrite -Heq. case: Hu2 => n Hu2 ; exists n ; by rewrite -Heq. move => M ; case: (Hu M) => {Hu} n Hu ; exists n ; by rewrite -Heq. move => M n ; by rewrite -Heq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy