proposition: Lemma Inf_eq_glb (u : nat -> Rbar) : Inf_seq u = Rbar_glb (fun x => exists n, x = u n).
proof: Proof. rewrite /Inf_seq ; case: (ex_inf_seq _) => /= s Hs. rewrite /Rbar_glb ; case: (Rbar_ex_glb _) => /= l Hl. apply (Rbar_is_glb_eq (fun x : Rbar => exists n : nat, x = u n) (fun x : Rbar => exists n : nat, x = u n)) => // ; by apply is_inf_seq_glb. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy