proposition: Lemma mlead_antisym_sorted (p : {mpoly R[n]}) : p \is antisym -> forall (i j : 'I_n), i <= j -> (mlead p) j <= (mlead p) i.
proof: Proof. Proof using. move=> sym_p i j le_ij; have [->|nz_p] := eqVneq p 0. by rewrite mlead0 !mnm0E. set m := mlead p; case: leqP=> // h. pose s := tperm i j; pose ms := m#s; have: (m < ms)%O. apply/ltmcP; first by rewrite mdeg_mperm. exists i=> [k lt_ki|]; last by rewrite mnmE tpermL. rewrite mnmE tpermD // neq_ltn orbC ?lt_ki //. by move/leq_trans: lt_ki => /(_ _ le_ij) ->. have: ms \in msupp p by rewrite isantisym_msupp // mlead_supp. by move/msupp_le_mlead; rewrite leNgt => /negbTE ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition