proposition: Lemma stdtab_of_yam_nil y : is_yam y -> [::] \notin (stdtab_of_yam y).
proof: Proof. move/stdtab_of_yamP; rewrite /is_stdtab => /andP[Htab _]. elim: (stdtab_of_yam) Htab => [// | t0 t IHt] /= /and4P[Hnnil _ _ {}/IHt H]. by rewrite inE negb_or eq_sym Hnnil H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau