proposition: Lemma cauchy_distance : forall {T : UniformSpace} {F} {FF : ProperFilter F}, cauchy F <-> (forall eps : posreal, exists P, F P /\ forall u v : T, P u -> P v -> ball u eps v).
proof: Proof. intros T F FF. split. - intros H eps. case: (H (pos_div_2 eps)) => {H} x Hx. exists (ball x (pos_div_2 eps)). split. by []. move => u v Hu Hv. rewrite (double_var eps). apply ball_triangle with x. by apply ball_sym. exact Hv. - intros H eps. case: (H eps) => {H} P [HP H]. destruct (filter_ex P HP) as [x Hx]. exists x. move: (fun v => H x v Hx) => {} H. apply filter_imp with (1 := H). by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub