proposition: Lemma sym_symmE (p : {sympoly R[n]}) : p = \sum_(m <- msupp p | m \is dominant) p@_m *: 'm[partm m].
proof: Proof. apply/eqP/symE => // m mdom; rewrite !raddf_sum /=. case: (boolP (m \in msupp p)) => [minsupp | mninsupp]. - rewrite -big_filter (bigD1_seq m) /=; first last. + by apply filter_uniq; apply msupp_uniq. + by rewrite mem_filter mdom. rewrite linearZ /= mcoeff_symm ?size_partm //. rewrite perm_sym partm_permK mulr1 big_seq_cond /=. rewrite big1 ?addr0 // => mon /andP[]. rewrite linearZ /= mcoeff_symm ?size_partm //. rewrite mem_filter => /andP[mondom monsupp] /eqP neq. case: (boolP (perm_eq _ _)) => [/permPr Hperm|]; last by rewrite mulr0. exfalso; apply: neq; apply: dominant_eq => //. by rewrite -{}Hperm partm_permK. - rewrite (memN_msupp_eq0 mninsupp); symmetry. rewrite big_seq_cond; apply big1 => /= m' /andP[Hsupp Hdom]. rewrite mcoeffZ (mcoeff_symm _ (size_partm _)) partmK //. suff -> : perm_eq m' m = false by rewrite mulr0. apply/negP => Hperm; move: mninsupp. by rewrite -(dominant_eq Hdom mdom Hperm) Hsupp. 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