proposition: Lemma filterlim_locally_unique : forall {F} {FF : ProperFilter' F} (f : T -> V) (x y : V), filterlim f F (locally x) -> filterlim f F (locally y) -> x = y.
proof: Proof. intros F FF f x y. apply is_filter_lim_unique. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub