proposition: Lemma symfnS (p : {mpoly R[n]}) : { n : nat | p \is symmetric -> (symfn n p).2 = 0 }.
proof: Proof. have: p \is symmetric -> { n : nat | (symfn n p).2 = 0 }. elim/mleadrect: p => p ih sym_p; case/and3P: (symf1P sym_p). case: ((symf1 p).2 =P 0)=> /= [z_q1|nz_q1]; first by exists 0%N. move=> le_q1 /ih -/(_ le_q1) [k z_q2] /eqP pE. exists k.+1=> /=; have E T U (z : T * U): z = (z.1, z.2) by case: z. by rewrite [symf1 _]E [symfn _ _]E z_q2. by case: (p \is symmetric)=> [[]// k eq|_]; [exists k | exists 0%N]. 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