proposition: Lemma ex_finite_lim_seq_correct (u : nat -> R) : ex_finite_lim_seq u <-> ex_lim_seq u /\ is_finite (Lim_seq u).
proof: Proof. split. case => l Hl. split. by exists l. by rewrite (is_lim_seq_unique _ _ Hl). case ; case => l Hl H. exists l. rewrite -(is_lim_seq_unique _ _ Hl). by rewrite H (is_lim_seq_unique _ _ Hl). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy