proposition: Lemma map_mpolyX (m : 'X_{1..n}) : map_mpoly mor 'X_[m] = 'X_[m].
proof: Proof. Proof using. by rewrite /= /map_mpoly mmapX /= /mmap1 mprodXnE -multinomUE_id. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition