proposition: Lemma expUmpartNE nv k i (P : intpartn k.+1) : ((U_(i) *+ k.+1)%MM == mpart P :> 'X_{1..nv.+1}) = (i == ord0) && (P == rowpartn k.+1).
proof: Proof. apply/eqP/andP => [| [/eqP ->{i} /eqP ->{P}]]; last exact: expUmpartE. rewrite /mpart; case: leqP => _; first last. move/(congr1 (fun mon : 'X_{1..nv.+1} => mon i)). by rewrite mulmnE !mnmE -val_eqE /= eqxx mul1n. case: (i =P ord0) => [->{i} | /eqP/negbTE neq H]; first split => //. apply/eqP/val_inj; rewrite /= rowpartnE. case: P H => [[|p0 [|p1 p]]]//=. by rewrite addn0 => /andP[/eqP ->]. rewrite -/(is_part (p1 :: p)) => /and3P[Hsum _ Hpart]. move/(congr1 (fun mon : 'X_{1..nv.+1} => mon ord0)). rewrite mulmnE !mnmE -val_eqE /= mul1n => Hp0; exfalso. move: Hsum Hpart; rewrite -{}Hp0 -{2}(addn0 k.+1) eqn_add2l. by rewrite addn_eq0 => /andP[/eqP-> _] /part_head_non0. exfalso; move/(congr1 (fun mon : 'X_{1..nv.+1} => mon ord0)): H. rewrite mulmnE !mnmE {}neq mul0n /= => Hp0. case: P Hp0 => [[//|p0 p]] Hp /= Hp0. by move: Hp; rewrite -{}Hp0 => /andP[_ /part_head_non0]. 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