proposition: Lemma isantisymP p : reflect (forall s, msym s p = (-1) ^+ s *: p) (p \is antisym).
proof: Proof. Proof using. by apply/(iffP forallP) => /= H s; apply/eqP/H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition