proposition: Lemma msuppX1 i : msupp 'X_i = [:: U_(i)%MM].
proof: Proof. Proof using. rewrite msuppE /= unlock /= domU //; exact: oner_neq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition