proposition: Lemma yam_of_stdtabP t : is_stdtab t -> is_yam (yam_of_stdtab t).
proof: Proof. move=> Hstdtab; have:= part_yam_of_stdtab Hstdtab. rewrite /yam_of_stdtab. move H : (size_tab t) => n. elim: n t H Hstdtab => [// | n IHn] t Hsize Hstdtab. move Hw : (to_word t) Hsize => w; case : w Hw => [// | w0 w]. by rewrite -size_to_word => -> /=. rewrite /= => Ht Hsize -> /=. have Hnnil : t != [::] by move: Hsize => /eqP; apply contraL => /eqP ->. have:= size_tab_remn Hstdtab Hnnil; rewrite Hsize /= => Hsz. apply (IHn _ Hsz); first exact: is_stdtab_remn. rewrite -Hsz. exact: part_yam_of_stdtab (is_stdtab_remn Hstdtab). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau