proposition: Lemma gauge_split A : gauge A -> exists2 B, gauge B & B \; B `<=` A.
proof: Proof. case => n _ EA; exists (iter n.+1 split_sym (E `&` E^-1)); first by exists n.+1. apply: subset_trans EA; apply: subset_trans; first last. by apply: subset_split_ent; exact: iter_split_ent. by case=> a c [b] [] ? ? [] ? ?; exists b. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed