proposition: Lemma alt_alternate (m : 'X_{1..n}) (i j : 'I_n) : i != j -> m i = m j -> 'a_m = 0.
proof: Proof. Proof using . move=> H Heq. pose t := tperm i j. have /= oddMt s : (t * s)%g = ~~ s :> bool by rewrite odd_permM odd_tperm H. rewrite [alternpol _](bigID (@odd_perm _)) /=. apply: canLR (subrK _) _; rewrite add0r -sumrN. rewrite (reindex_inj (mulgI t)); apply: eq_big => //= s. rewrite oddMt => /negPf ->; rewrite scaleN1r scale1r; congr (- _). rewrite msymMm. suff -> : msym t 'X_[m] = 'X_[m] :> {mpoly R[n]} by []. rewrite msymX; congr mpolyX. rewrite mnmP => k /=. rewrite !mnmE /= tpermV. by case: (tpermP i j k) => Hk //; rewrite Hk Heq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition mathcomp(matrix)