proposition: Lemma is_part_skew_yam sha shb y : is_part sha -> is_skew_yam sha shb y -> is_part shb.
proof: Proof. move=> /hyper_yam_of_eval Ha /(_ _ Ha). by rewrite /is_yam_of_eval => /andP[/is_part_eval_yam H /eqP<-]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab