proposition: Lemma symfnP k (p : {mpoly R[n]}) : p \is symmetric -> [&& ((symfn k p).2 == 0) || (mlead (symfn k p).2 < mlead p)%O , (symfn k p).2 \is symmetric & p == (symfn k p).1 \mPo S + (symfn k p).2].
proof: Proof. elim: k p=> [|k ih] p sym_p /=; first exact/symf1P. have E T U (z : T * U) : z = (z.1, z.2) by case: z. rewrite [symf1 p]E [symfn _ _]E /= => {E}. case/and3P: (symf1P sym_p); case/orP=> [/eqP-> _ /eqP pE|]. by rewrite symfnE0 /= eqxx rpred0 /= {1}pE !simpm. move=> le_q1_p /ih /and3P[]; case/orP=> [/eqP-> _|]. move=> /eqP q1E /eqP pE; rewrite eqxx rpred0 /=. by rewrite {1}pE {1}q1E !simpm /= addr0 raddfD. move=> le_q2_q1 -> /eqP q1E /eqP pE. rewrite (lt_trans le_q2_q1) ?orbT //= {1}pE {1}q1E. by rewrite addrA raddfD. 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