proposition: Lemma size_notin_stdtab_of_yam y : (size y) \notin (to_word (stdtab_of_yam y)).
proof: Proof. have:= std_of_yam y. rewrite /is_std size_to_word size_stdtab_of_yam => /perm_mem ->. by rewrite mem_iota add0n /= ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau