proposition: Lemma Lim_correct (f : R -> R) (x : Rbar) : ex_lim f x -> is_lim f x (Lim f x).
proof: Proof. intros (l,H). replace (Lim f x) with l. apply H. apply sym_eq, is_lim_unique, H. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq