proposition: Lemma perm_join_tab s t : size s <= size t -> perm_eq (to_word (join_tab s t)) (to_word s ++ to_word t).
proof: Proof. Proof using. rewrite /join_tab /=. elim: t s => [// | t0 t IHt] /= s; first by rewrite leqn0 => /nilP -> /=. case: s => [_ | s0 s] /=. rewrite !to_word_cons {IHt}. rewrite [map _ _](_ : _ = t); first by exact: perm_refl. by elim: t {t0} => [// | t0 t] /= ->. rewrite ltnS subSS => {}/IHt. rewrite !to_word_cons -!/(to_word _) !catA perm_cat2r. move: (map _ _) => m. rewrite -(perm_cat2r s0) => /perm_trans; apply. rewrite -!catA perm_cat2l. apply/permPl; exact: perm_catC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab