proposition: Lemma sym_fundamental (p : {mpoly R[n]}) : p \is symmetric -> { t | t \mPo S = p /\ mweight t <= msize p}.
proof: Proof. by exists (symf p); rewrite {2}[p]symfP ?symfn_wgle. 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