proposition: Lemma stdtab_of_yam_inj x y : is_yam x -> is_yam y -> stdtab_of_yam x = stdtab_of_yam y -> x = y.
proof: Proof. move=> Hx Hy Heq; have:= congr1 size_tab Heq. rewrite !size_stdtab_of_yam => Hsz. elim: x y Hsz Heq Hx Hy => [| x0 x IHx]; case=> [| y0 y] //= /eqP. rewrite eqSS => /eqP Heqsz; rewrite Heqsz => Heq. have Hfind w := find_append_nth _ (size_notin_stdtab_of_yam w). have:= Hfind x0 x; rewrite Heqsz Heq {}Hfind => H0. move=> /andP[_ Hx] /andP[_ Hy]. rewrite H0; congr (_ :: _); move: Heqsz => {}/IHx; apply => //. move: Heq; rewrite {}H0. by apply: append_nth_injl; apply: stdtab_of_yam_nil. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau