proposition: Lemma symfn_wgle k (p : {mpoly R[n]}) : p \is symmetric -> mweight (symfn k p).1 <= msize p.
proof: Proof. elim: k p => [|k ih] p sym_p /=; first exact/symf1_wgle. 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 /= addr0; apply/symf1_wgle. move=> le_q1_p sym_q2 /eqP pE. rewrite (leq_trans (mmeasureD_le _ _ _)) //. rewrite geq_max symf1_wgle //= (leq_trans (ih _ _)) //. have [->|nz_p] := eqVneq p 0; first by rewrite symf1E0 msize0. have [->|nz_f1p] := eqVneq (symf1 p).2 0; first by rewrite msize0. by rewrite -!mlead_deg // ltnS lemc_mdeg // ltW. 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