proposition: Lemma complete_cauchy : forall F : (T -> Prop) -> Prop, ProperFilter F -> cauchy F -> forall eps : posreal, F (ball (lim F) eps).
proof: Proof. apply CompleteSpace.ax1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub