proposition: Fact symp_sym d : symp_pol d \is symmetric.
proof: Proof. Proof using. apply/issymP => s. rewrite linear_sum /= (reindex_inj (perm_inj (s := s^-1)))%g /=. apply eq_bigr => i _; rewrite rmorphXn /=; congr (_ ^+ _). rewrite msymX /=; congr mpolyX. rewrite mnmP => j; rewrite !mnmE /=; congr nat_of_bool. by apply/eqP/eqP => [|->//]; apply: perm_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