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