proposition: Lemma size_join_tab s t : size s <= size t -> size_tab (join_tab s t) = size_tab s + size_tab t.
proof: Proof. Proof using. rewrite /join_tab /size_tab. elim: s t => [| s0 s IHs] /= t. by rewrite add0n subn0; elim: t => //= t0 t /= ->. case: t => //= t0 t. rewrite ltnS subSS => {}/IHs ->. rewrite size_cat -!addnA; congr (_ + _). by rewrite addnA addnAC addnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab