proposition: Lemma Lim_seq_correct (u : nat -> R) : ex_lim_seq u -> is_lim_seq u (Lim_seq u).
proof: Proof. intros (l,H). cut (Lim_seq u = l). intros ; rewrite H0 ; apply H. apply is_lim_seq_unique, H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy