proposition: Theorem yam_of_stdtabK t : is_stdtab t -> stdtab_of_yam (yam_of_stdtab t) = t.
proof: Proof. rewrite /yam_of_stdtab. move H : (size_tab t) => n. elim: n t H => [| n IHn] t. by rewrite /is_stdtab => /= /tab0 H /andP[/H ->]. move=> Hsize Hstdtab /=. have Hnnil : t != [::] by move: Hsize => /eqP; apply contraL => /eqP ->. have:= size_tab_remn Hstdtab Hnnil. rewrite Hsize /= => /(IHn (remn t)) {IHn} Hrec. rewrite (Hrec (is_stdtab_remn Hstdtab)) size_yam_of_stdtab_rec. by have:= append_nth_remn Hstdtab Hnnil; rewrite Hsize /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau