proposition: Lemma is_LimSup_LimInf_lim_seq (u : nat -> R) (l : Rbar) : is_LimSup_seq u l -> is_LimInf_seq u l -> is_lim_seq u l.
proof: Proof. case: l => [l | | ] /= Hs Hi ; apply is_lim_seq_spec. move => eps. case: (proj2 (Hs eps)) => {Hs} Ns Hs. case: (proj2 (Hi eps)) => {Hi} Ni Hi. exists (Ns + Ni)%nat => n Hn. apply Rabs_lt_between' ; split. apply Hi ; intuition. apply Hs ; intuition. exact Hi. exact Hs. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy