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