proposition: Lemma join_stdtab s t : is_stdtab s -> is_skew_tableau (shape s) t -> is_tableau (join_tab s (map (shiftn (size_tab s)) t)).
proof: Proof. rewrite /is_stdtab => /andP[]. rewrite /is_std size_to_word /= => Htabs Hperm /(is_skew_tableau_map_shiftn (size_tab s)). apply: join_tab_skew; last exact Htabs. rewrite {2}/to_word -map_rev -map_flatten. move: (flatten (rev t)) => w. apply/allP => x /mapP[i _ ->{x}]. rewrite /allLtn; apply/allP => j. rewrite (perm_mem Hperm) mem_iota /= add0n ltEnat => /leq_trans; apply. exact: leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools ordcast combclass partition skewpart Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur