proposition: Lemma sym_VanprodM n (R : comRingType) (p : {mpoly R[n]}) : p \is symmetric -> Vanprod * p \is antisym.
proof: Proof. by apply sym_anti; apply Vanprod_anti. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition