proposition: Lemma is_lim_Reals (f : R -> R) (x l : R) : is_lim f x l <-> limit1_in f (fun y => y <> x) l x.
proof: Proof. split ; [apply is_lim_Reals_0|apply is_lim_Reals_1]. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq