proposition: Lemma mx_ent_refl A : mx_ent A -> [set MN | MN.1 = MN.2] `<=` A.
proof: Proof. move=> [B entB sBA] MN MN1e2; apply: sBA => i j. by rewrite MN1e2; apply: entourage_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed