proposition: Lemma LimSup_LimInf_seq_le (u : nat -> R) : Rbar_le (LimInf_seq u) (LimSup_seq u).
proof: Proof. rewrite /LimInf_seq ; case: ex_LimInf_seq => /= li Hli. rewrite /LimSup_seq ; case: ex_LimSup_seq => /= ls Hls. by apply is_LimSup_LimInf_seq_le with u. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy