proposition: Lemma cnvar_leq_symeE i : i <= m -> cnvarsym 'e_i = 'e_i.
proof: Proof. move=> Hi; apply val_inj; rewrite /= /sympolyf. case: (SF 'e_i) => /= p [Hp _]. case: i Hi Hp => [_ |i Hi Hp] /=. rewrite !mesym0E /= => Hp. have {Hp} -> : p = 1 by apply msym_fundamental_un; rewrite Hp comp_mpoly1. by rewrite comp_mpoly1. have {Hp} -> : p = 'X_(Ordinal Hi). apply msym_fundamental_un; rewrite Hp comp_mpolyXU. by rewrite -tnth_nth tnth_mktuple. by rewrite comp_mpolyXU -tnth_nth tnth_mktuple. 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