proposition: Lemma skew_yam_included sha shb y : is_part sha -> is_skew_yam sha shb y -> included sha shb.
proof: Proof. move=> Hpart. elim: y shb => [| y0 y IHy] shb /= Hskew. move/(_ _ (hyper_yam_of_eval Hpart)) : Hskew. rewrite cat0s /is_yam_of_eval (evalseq_hyper_yam Hpart) => /andP[_ /eqP->]. exact: included_refl. move/(_ _ (skew_yam_consK Hpart Hskew)) : IHy => Hrec. have/(_ _ (hyper_yam_of_eval Hpart)) := Hskew. rewrite /is_yam_of_eval => /andP[/is_rem_corner_yam Hcorn /eqP Hb]. rewrite Hb in Hcorn. have:= included_incr_nth (decr_nth shb y0) y0. rewrite (decr_nthK (is_part_skew_yam Hpart Hskew) Hcorn). exact: included_trans. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab