proposition: Lemma mons2mE s : 'X_[s2m s] = \prod_(i <- s) 'X_i :> {mpoly R[n]}.
proof: Proof. rewrite /s2m; elim: s => [| s0 s IHs]/=. by rewrite big_nil -/mnm0 mpolyX0. rewrite big_cons -{}IHs -mpolyXD; congr ('X_[_]). by rewrite mnmP => i; rewrite mnmDE !mnmE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau