proposition: Theorem Vanprod_alt_int n : Vanprod = alternpol 'X_[rho n] :> {mpoly int[n]}.
proof: Proof. rewrite (isantisym_alt _ (Vanprod_neq0 n _) (Vanprod_anti _ _) (Vanprod_dhomog n _)). - by rewrite Vanprod_coeff_rho scale1r. - by apply/negP => /=; rewrite inE /= eqz_nat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition