proposition: Lemma Rbar_sup_eq_lub (u : nat -> Rbar) : Sup_seq u = Rbar_lub (fun x => exists n, x = u n).
proof: Proof. rewrite /Sup_seq ; case: (ex_sup_seq _) => /= s Hs. rewrite /Rbar_lub ; case: (Rbar_ex_lub _) => /= l Hl. apply (Rbar_is_lub_eq (fun x : Rbar => exists n : nat, x = u n) (fun x : Rbar => exists n : nat, x = u n)) => // ; by apply is_sup_seq_lub. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy