proposition: Lemma mcoeff_alt (m : 'X_{1..n}) : uniq m -> ('a_m)@_m = 1.
proof: Proof. move=> Huniq. rewrite /alternpol (reindex_inj invg_inj) /=. rewrite raddf_sum /= (bigID (pred1 1%g)) /=. rewrite big_pred1_eq odd_permV odd_perm1 expr0 scale1r invg1 msym1m. rewrite mcoeffX eq_refl /=. rewrite big1 ?addr0 // => /= s Hs. rewrite mcoeffZ msymX mcoeffX invgK. suff : [multinom m (s i) | i < n] != m by move=> /negbTE ->; rewrite mulr0. move: Hs; apply contra => /eqP; rewrite mnmP => Heq. apply/eqP; rewrite -permP => i; rewrite perm1; apply val_inj => /=. have /eqP := Heq i; rewrite !mnmE !(mnm_nth 0). rewrite nth_uniq; last exact: Huniq. - by move=> /eqP ->. - rewrite size_tuple; exact: ltn_ord. - rewrite size_tuple; exact: ltn_ord. 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)