proposition: Lemma symE (p q : {sympoly R[n]}) : reflect (forall m, m \is dominant -> p@_m = q@_m) (p == q).
proof: Proof. apply (iffP eqP) => [-> //| Hdom]; apply/val_inj/mpolyP => m /=. have [s /eqP <- ] := perm_mpart_partm m. rewrite -(issymP p (sympolP p) (s^-1)%g) -(issymP q (sympolP q) (s^-1)%g). rewrite !mcoeff_sym mpermKV. by apply: Hdom; apply/mpart_is_dominant. 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