proposition: Lemma isantisym_msupp_uniq (m : 'X_{1..n}) : m \in msupp p -> uniq m.
proof: Proof. Proof using Hchar Hpanti. rewrite mcoeff_msupp => Hsupp. case: (boolP (uniq m)) => // /uniqPn => /(_ 0%N). move=> [i] [j] []; rewrite size_tuple => Hi Hj Hnth. move/isantisymP/(_ (tperm (Ordinal (ltn_trans Hi Hj)) (Ordinal Hj))) : Hpanti. rewrite odd_tperm /eq_op /=. rewrite (ltn_eqF Hi) expr1 scaleN1r. move/(congr1 (mcoeff m)); rewrite mcoeffN mcoeff_sym. have -> : m#tperm (Ordinal (ltn_trans Hi Hj)) (Ordinal Hj) = m. rewrite mnmP => k; rewrite mnmE. by case: (tpermP _ _ k) => [-> | -> |] //; rewrite !(mnm_nth 0) /= Hnth. move/eqP; rewrite -addr_eq0. rewrite -mulr2n -mulr_natr mulf_eq0. move: Hchar; rewrite negb_and => /negbTE ->. by move: Hsupp => /negbTE ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition