proposition: Lemma iota_is_filter_lim {F} {FF : ProperFilter' F} (l : V) : is_filter_lim F l -> iota (is_filter_lim F) = l.
proof: Proof. intros Hl. apply: iota_unique (Hl) => l' Hl'. exact: is_filter_lim_unique Hl' Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub