proposition: Lemma symf1P (p : {mpoly R[n]}) : p \is symmetric -> [&& ((symf1 p).2 == 0) || (mlead (symf1 p).2 < mlead p)%O , (symf1 p).2 \is symmetric & p == (symf1 p).1 \mPo S + (symf1 p).2].
proof: Proof. rewrite /symf1; case: (eqVneq p 0) => [->|nz_p sym_p] /=. by rewrite comp_mpoly0 addr0 eqxx andbT. rewrite addrCA comp_mpolyZ subrr addr0 eqxx andbT rpredB //; last first. by apply/rpredZ/mcomp_sym => i; rewrite -tnth_nth tnth_map; apply/mesym_sym. case: eqVneq; rewrite //= andbT. have := mlead_XLS (mlead_msym_sorted sym_p). set c := nth 0%N (mlead p); pose F i := (c i - c i.+1)%N. rewrite -/(F#val) => mE. set q : {mpoly R[n]} := p@_(mlead p) *: (_ \mPo _). rewrite lt_neqAle andbC /= => nz_pBq. have := mleadB_le p q; rewrite mleadZ_proper; last first. by rewrite mE mulrC mulrI_eq0 ?mleadc_eq0 // -mE mleadc_XS; apply/lreg1. rewrite mE joinxx => -> /=; apply/contraTneq: nz_pBq. rewrite -mleadc_eq0 => ->; rewrite /q mcoeffB mcoeffZ -{3}mE. by rewrite mleadc_XS mulr1 subrr eqxx. 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