proposition: Lemma gauge_countable_uniformity : countable_uniformity gauged.
proof: Proof. exists [set iter n split_sym (E `&` E^-1) | n in [set: nat]]. split; [exact: card_image_le | by move=> W [n] _ <-; exists n|]. by move=> D [n _ ?]; exists (iter n split_sym (E `&` E^-1)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed