proposition: Lemma eq_mnm1 (i j : 'I_n) : (U_(i)%MM == U_(j)%MM) = (i == j).
proof: Proof. case: (i =P j) => [-> | /eqP/negbTE neq]; first by rewrite eqxx. apply/negbTE/negP => /eqP; rewrite mnmP => /(_ j). by rewrite !mnm1E eqxx neq. 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