proposition: Lemma skew_dominate_cut sh u v : skew_dominate sh u v = skew_dominate sh u (take (size u - sh) v).
proof: Proof. Proof using. rewrite /skew_dominate /=. apply/idP/idP. - move=> Hdom; have/dominateP[Hsz _] := Hdom. move: Hdom; rewrite -{1}(cat_take_drop (size u - sh) v). apply dominate_cut. move: Hsz; rewrite size_drop size_take -/(minn _ _). by rewrite minnC /minn ltnNge => ->. - exact: dominate_take. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab