proposition: Lemma ex_lim_continuity (f : R -> R) (x : R) : continuity_pt f x -> ex_finite_lim f x.
proof: Proof. move => Hf. exists (f x). by apply is_lim_continuity. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq