proposition: Lemma symf1_wgle (p : {mpoly R[n]}) : p \is symmetric -> mweight (symf1 p).1 <= msize p.
proof: Proof. move=> sym_p; rewrite /symf1; case: (p =P 0). by rewrite mmeasure0. move=> /eqP nz_p; set X := 'X_[_] => /=. rewrite (@leq_trans (mweight X)) ?mmeasureZ_le //. rewrite -?mlead_deg ?mleadc_eq0 // mweight_XLS //. exact/mlead_msym_sorted. 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