proposition: Lemma omegasf_compsymh p q : (sympol p == q \mPo [tuple sympol 'h_i.+1 | i < n]) = (sympol (omegasf p) == q \mPo [tuple sympol 'e_i.+1 | i < n]).
proof: Proof. rewrite -(omegasf_sympolyf_eval q); apply/eqP/eqP => [/val_inj ->| Heq]. - by rewrite omegasfK sympolyf_evalE. - have {Heq} /(congr1 omegasf) : omegasf p = sympolyf_eval q. by apply: sympol_inj; rewrite Heq sympolyf_evalE. by rewrite omegasfK => ->. 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