fact: Definition Vanprod {n} {R : ringType} : {mpoly R[n]} := \prod_(p : 'II_n | p.1 < p.2) ('X_p.1 - 'X_p.2).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition