proposition: Lemma ex_finite_lim_correct (f : R -> R) (x : Rbar) : ex_finite_lim f x <-> ex_lim f x /\ is_finite (Lim f x).
proof: Proof. split. case => l Hf. move: (is_lim_unique f x l Hf) => Hf0. split. by exists l. by rewrite Hf0. case ; case => l Hf Hf0. exists (real l). rewrite -(is_lim_unique _ _ _ Hf). rewrite Hf0. by rewrite (is_lim_unique _ _ _ Hf). Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq