proposition: Lemma R_complete_close : forall F1 F2 : (R -> Prop) -> Prop, filter_le F1 F2 -> filter_le F2 F1 -> close (R_complete_lim F1) (R_complete_lim F2).
proof: Proof. intros F1 F2 H12 H21. replace (R_complete_lim F2) with (R_complete_lim F1). intros eps. apply ball_center. exact: R_complete_ax2. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub