proposition: Lemma is_filter_lim_locally_unique : forall (x y : V), is_filter_lim (locally x) y -> x = y.
proof: Proof. intros x y H. apply eq_close. now apply is_filter_lim_locally_close. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub