proposition: Lemma mxOverS (S1 S2 : {pred T}) : {subset S1 <= S2} -> {subset mxOver S1 <= mxOver S2}.
proof: Proof. by move=> sS12 M /mxOverP S1M; apply/mxOverP=> i j; apply/sS12/S1M. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)