proposition: Lemma skew_yam_catK sha shc y z : is_part sha -> is_skew_yam sha shc (y ++ z) -> { shb | is_skew_yam sha shb z & is_skew_yam shb shc y }.
proof: Proof. move=> Hpart. elim: y z shc => [| y0 y IHy ] z shc Hz /=. exists shc; first exact: Hz. exact: skew_yam_nil. move/(_ _ _ (skew_yam_consK Hpart Hz)) : IHy => [shb] Hskz Hy. exists shb; first exact: Hskz. exact: (skew_yam_catrK Hpart Hskz Hz). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab