proposition: Lemma isantisym_msupp p (s : 'S_n) (m : 'X_{1..n}) : p \is antisym -> (m#s \in msupp p) = (m \in msupp p).
proof: Proof. Proof using. rewrite !mcoeff_msupp -mcoeff_sym => /isantisymP ->. case: (odd_perm s); last by rewrite expr0 scale1r. rewrite expr1 scaleN1r !mcoeff_eq0. by rewrite (perm_mem (msuppN _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition