proposition: Lemma skew_yam_catrK sha shb shc y z : is_part sha -> is_skew_yam sha shb y -> is_skew_yam sha shc (z ++ y) -> is_skew_yam shb shc z.
proof: Proof. move=> /hyper_yam_of_eval Ha Hy Hcat. apply (is_skew_yamE (Hy _ Ha)). rewrite catA; exact: Hcat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab