proposition: Lemma mx_ent_filter : Filter mx_ent.
proof: Proof. apply: filter_from_filter => [|A B entA entB]. by exists (fun _ _ => setT) => _ _; apply: filterT. exists (fun i j => A i j `&` B i j); first by move=> ??; apply: filterI. by move=> MN ABMN; split=> i j; have [] := ABMN i j. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed