proposition: Lemma alt_uniq_non0 (m : 'X_{1..n}) : uniq m -> 'a_m != 0.
proof: Proof. Proof using . move=> Huniq. suff : mcoeff m 'a_m == 1. apply contraL => /eqP ->; rewrite mcoeff0 eq_sym. exact: oner_neq0. by rewrite mcoeff_alt. 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)