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