proposition: Lemma symm_unique d (f : {sympoly R[n]}) c : f = \sum_(l : 'P_d) (c l) *: 'm[l] -> forall l : 'P_d, size l <= n -> c l = f@_(mpart l).
proof: Proof. move=> -> l Hl. rewrite !linear_sum /=. rewrite (bigD1 l) //= !linearZ /= (mcoeff_symm _ Hl) perm_refl /= mulr1. rewrite big1 ?addr0 // => i Hil /=. case: (leqP (size i) n) => [Hi | /symm_oversize ->]; last by rewrite scaler0 mcoeff0. rewrite linearZ /= mcoeff_symm //. rewrite [perm_eq _ _](_ : _ = false) /= ?mulr0 //. apply negbTE; move: Hil; apply contra. move=> /perm_partm/(congr1 pval). rewrite !mpartK // => Hil. by apply/eqP/val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv