proposition: Lemma is_filter_lim_close {F} {FF : ProperFilter F} (x y : T) : is_filter_lim F x -> is_filter_lim F y -> close x y.
proof: Proof. intros Hx Hy eps. specialize (Hy _ (locally_ball y (pos_div_2 eps))). specialize (Hx _ (locally_ball x (pos_div_2 eps))). generalize (filter_and _ _ Hx Hy) => {Hx Hy} H. destruct (filter_ex _ H) as [z Hz]. rewrite (double_var eps). apply ball_triangle with z. apply Hz. apply ball_sym, Hz. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub