proposition: Lemma stdtab_of_yamP y : is_yam y -> is_stdtab (stdtab_of_yam y).
proof: Proof. rewrite /is_stdtab std_of_yam andbT. elim: y => [// | y0 y IHy] /= /andP[Hpart {}/IHy]. move: Hpart; rewrite -shape_stdtab_of_yam. suff : all (gtn (size y)) (to_word (stdtab_of_yam y)) by apply: is_tab_append_nth_size. have:= std_of_yam y; rewrite /is_std size_to_word size_stdtab_of_yam. move=> /perm_mem Hperm. apply/allP => x Hx /=. by move/(_ x) : Hperm; rewrite mem_iota /= add0n Hx => /esym ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau