proposition: Theorem stdtab_of_yamK y : is_yam y -> yam_of_stdtab (stdtab_of_yam y) = y.
proof: Proof. move=> Hyam. have /yam_of_stdtabK := (stdtab_of_yamP Hyam). apply: stdtab_of_yam_inj; last exact Hyam. by apply: yam_of_stdtabP; apply: stdtab_of_yamP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau