proposition: Lemma cauchy_exP (R : numFieldType) (T : pseudoMetricType R) (F : set_system T) (FF : Filter F) : cauchy_ex F -> cauchy F.
proof: Proof. move=> Fc A; rewrite !nbhs_simpl /= -entourage_ballE => -[_/posnumP[e] sdeA]. have /Fc [z /= Fze] := [gt0 of e%:num / 2]; near=> x y; apply: sdeA => /=. by apply: (@ball_splitr _ _ z); [near: x|near: y]. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed