proposition: Lemma yam_tail_non_nil (l : nat) (s : seq nat) : is_yam (l.+1 :: s) -> s != [::].
proof: Proof. Proof using. case: s => [| //] Hyam. by have:= is_part_eval_yam Hyam; rewrite part_head0F. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab