proposition: Lemma skew_dominate_no_overlap sh u v : size u <= sh -> skew_dominate sh u v.
proof: Proof. Proof using. by rewrite /skew_dominate => /drop_oversize ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab