proposition: Lemma cauchyP (R : numFieldType) (T : pseudoMetricType R) (F : set_system T) (PF : ProperFilter F) : cauchy F <-> cauchy_ex F.
proof: Proof. split=> [Fcauchy _/posnumP[e] |/cauchy_exP//]. near F => x; exists x; near: x; apply: (@nearP_dep _ _ F F). exact/Fcauchy/entourage_ball. 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