proposition: Lemma Rbar_is_glb_inf_seq (u : nat -> Rbar) (l : Rbar) : Rbar_is_glb (fun x => exists n, x = u n) l -> is_inf_seq u l.
proof: Proof. move => H ; apply is_sup_opp_inf_seq ; apply Rbar_is_lub_sup_seq ; apply Rbar_glb_lub. rewrite Rbar_opp_involutive ; apply (Rbar_is_glb_ext (fun x : Rbar => exists n : nat, x = u n)) => // x ; split ; case => n Hx ; exists n ; by apply Rbar_opp_eq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy