proposition: Lemma is_lim_continuity (f : R -> R) (x : R) : continuity_pt f x -> is_lim f x (f x).
proof: Proof. intros cf. now apply continuity_pt_filterlim'. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq