proposition: Lemma skew_nil_yamE eval y : is_yam_of_eval eval y -> is_skew_yam [::] eval y.
proof: Proof. move=> Hy z; rewrite {1}/is_yam_of_eval => /andP[_ /eqP Hz]. have:= evalseq_eq_size z; rewrite Hz /= => /esym/eqP/nilP ->. by rewrite cats0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab