proposition: Lemma ex_LimSup_seq (u : nat -> R) : {l : Rbar | is_LimSup_seq u l}.
proof: Proof. case: (ex_inf_seq (fun m : nat => Sup_seq (fun n : nat => u (n + m)%nat))) => l Hl. exists l. by apply is_LimSup_infSup_seq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy