proposition: Lemma skew_yam_cat sha shb shc y z : is_skew_yam sha shb y -> is_skew_yam shb shc z -> is_skew_yam sha shc (z ++ y).
proof: Proof. by rewrite /is_skew_yam => Hy Hz x /Hy /Hz; rewrite catA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab