proposition: Lemma cvg_cauchy {T : uniformType} (F : set_system T) : Filter F -> [cvg F in T] -> cauchy F.
proof: Proof. move=> FF cvF A entA; have /entourage_split_ex [B entB sB2A] := entA. exists (to_set ((B^-1)%classic) (lim F), to_set B (lim F)). split=> /=; apply: cvF; rewrite /= -nbhs_entourageE; last by exists B. by exists (B^-1)%classic => //; apply: entourage_inv. by move=> ab [/= Balima Blimb]; apply: sB2A; exists (lim F). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed