proposition: Corollary Vanprod_neq0 : Delta != 0.
proof: Proof. Proof using. apply/negP => /eqP H. have:= Vanprod_coeff_rho; rewrite {}H mcoeff0 => /esym/eqP. by rewrite oner_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition