proposition: Lemma mx_nbhs_filter M : ProperFilter (nbhs M).
proof: Proof. apply: (filter_from_proper (filter_from_filter _ _)) => [|P Q M_P M_Q|P M_P]. - by exists (fun i j => setT) => ??; apply: filterT. - exists (fun i j => P i j `&` Q i j) => [??|mx PQmx]; first exact: filterI. by split=> i j; have [] := PQmx i j. - exists (\matrix_(i, j) get (P i j)) => i j; rewrite mxE; apply: getPex. exact: filter_ex (M_P 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