proposition: Lemma Lim_correct' (f : R -> R) (x : Rbar) : ex_finite_lim f x -> is_lim f x (real (Lim f x)).
proof: Proof. intro Hf. apply ex_finite_lim_correct in Hf. rewrite (proj2 Hf). by apply Lim_correct, Hf. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq