proposition: Lemma std_of_yam y : is_std (to_word (stdtab_of_yam y)).
proof: Proof. rewrite /is_std size_to_word size_stdtab_of_yam. elim: y => [// | y0 y IHy]. have -> : iota 0 (size (y0 :: y)) = rcons (iota 0 (size y)) (size y). rewrite [size (y0 :: y)]/= -addn1 iotaD add0n /=. exact: cats1. apply: (perm_trans (perm_append_nth _ _ _)). move: IHy; rewrite -(perm_cons (size y)) => /perm_trans; apply. by rewrite perm_sym; apply/permPl; apply: perm_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau