proposition: Lemma ex_lim_LimSup_LimInf_seq (u : nat -> R) : ex_lim_seq u <-> LimSup_seq u = LimInf_seq u.
proof: Proof. split => Hl. case: Hl => l Hu. transitivity l. apply is_LimSup_seq_unique. by apply is_lim_LimSup_seq. apply sym_eq, is_LimInf_seq_unique. by apply is_lim_LimInf_seq. exists (LimSup_seq u). apply is_LimSup_LimInf_lim_seq. rewrite /LimSup_seq ; by case: ex_LimSup_seq. rewrite Hl /LimInf_seq ; by case: ex_LimInf_seq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy