proposition: Lemma mlead_msym_sorted (p : {mpoly R[n]}) : p \is symmetric -> forall (i j : 'I_n), i <= j -> (mlead p) j <= (mlead p) i.
proof: Proof. 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 issym_msupp // mlead_supp. by move/msupp_le_mlead; rewrite leNgt => /negbTE=> ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg