proposition: Lemma shape_join_tab s t : shape (join_tab s t) = ([seq pr.1 + pr.2 | pr <- zip (pad 0 (size t) (shape s)) (shape t)])%N.
proof: Proof. Proof using . rewrite /shape /join_tab -map_comp. rewrite (eq_map (g := (fun p => p.1 + p.2) \o (fun p => (size p.1, size p.2)))); first last. by move=> [a b] /=; rewrite size_cat. rewrite map_comp; congr map. elim: t s => [| t0 t IHt] [| s0 s] //=. by have /= := (IHt [::]); rewrite subn0 => ->. by rewrite IHt /= subSS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab