proposition: Lemma is_lim_Reals_1 (f : R -> R) (x l : R) : limit1_in f (fun y => y <> x) l x -> is_lim f x l.
proof: Proof. intros H. apply is_lim_spec. intros [e He]. destruct (H e He) as [d [Hd H']]. exists (mkposreal d Hd). intros y Hy Hxy. apply (H' y). now split. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq