proposition: Corollary Vanprod_alt n (R : ringType) : Vanprod = alternpol 'X_[rho n] :> {mpoly R[n]}.
proof: Proof. have := Vanprod_alt_int n => /(congr1 (map_mpoly (S := R) intr)). rewrite /Vanprod raddf_sum rmorph_prod. under [LHS]eq_bigr => p _ do rewrite raddfB /= !map_mpolyX /=. by move ->; apply eq_bigr => s _; rewrite raddfZsign !msymX /= map_mpolyX. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition