proposition: Lemma R_complete : forall F : (R -> Prop) -> Prop, ProperFilter F -> (forall eps : posreal, exists x : R, F (ball x eps)) -> forall eps : posreal, F (ball (R_complete_lim F) eps).
proof: Proof. intros F FF. apply R_complete_ax1. by apply Proper_StrongProper. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub