fact: Definition Lim_seq (u : nat -> R) : Rbar := Rbar_div_pos (Rbar_plus (LimSup_seq u) (LimInf_seq u)) {| pos := 2; cond_pos := Rlt_R0_R2 |}.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy