proposition: Lemma mx_ent_split A : mx_ent A -> exists2 B, mx_ent B & B \; B `<=` A.
proof: Proof. move=> [B entB sBA]. have Bsplit : forall i j, exists C, entourage C /\ C \; C `<=` B i j. by move=> ??; apply/exists2P/entourage_split_ex. exists [set MN : 'M[T]_(m, n) * 'M[T]_(m, n) | forall i j, get [set C | entourage C /\ C \; C `<=` B i j] (MN.1 i j, MN.2 i j)]. by exists (fun i j => get [set C | entourage C /\ C \; C `<=` B i j]). move=> MN [P CMN1P CPMN2]; apply/sBA => i j. have /getPex [_] := Bsplit i j; apply; exists (P i j); first exact: CMN1P. exact: CPMN2. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed