proposition: Lemma close_lim : forall F1 F2 : (T -> Prop) -> Prop, filter_le F1 F2 -> filter_le F2 F1 -> close (lim F1) (lim F2).
proof: Proof. apply CompleteSpace.ax2. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub