proposition: Lemma symhe1E : 'h_1 = 'e_1.
proof: Proof. Proof using. apply val_inj; rewrite syme1 /= -mpolyP => m. rewrite !raddf_sum /=. case: (boolP (mdeg m == 1%N)) => [/mdeg1P[i /eqP ->] | Hm]. - have Hdm : (mdeg U_(i))%MM < 2 by rewrite mdeg1. rewrite (bigD1 (BMultinom Hdm)) /=; last by rewrite mdeg1. rewrite mcoeffX eq_refl big1; first last. move=> mm /andP[_ /negbTE]. by rewrite mcoeffX {1}/eq_op /= => ->. rewrite /= (bigD1 i) // mcoeffX eq_refl /= big1 // => j /negbTE H. rewrite mcoeffX. case eqP => //; rewrite mnmP => /(_ i). by rewrite !mnm1E H eq_refl. - rewrite big1; first last. move=> p /eqP Hp; rewrite mcoeffX. case eqP => // Hpm; subst m. by move: Hm; rewrite Hp. rewrite big1 // => p _. rewrite mcoeffX; case eqP => // Hmm; subst m. by rewrite mdeg1 in Hm. 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