proposition: Lemma join_stdtab_in_shuffle s t : is_stdtab s -> size s <= size t -> to_word (join_tab s (map (shiftn (size_tab s)) t)) \in shsh (to_word s) (to_word t).
proof: Proof. rewrite /join_tab /is_stdtab => /andP[_ Hstd] Hsize. rewrite (mem_shsh _ _ Hstd). move: Hstd; rewrite /is_std size_to_word /= => Hperm. have {Hperm} : all (gtn (size_tab s)) (to_word s). apply/allP => i; rewrite (perm_mem Hperm). by rewrite mem_iota /= add0n. move: (size_tab s) => sh. rewrite /shiftn => Hall; apply /andP; split; apply/eqP. - elim: s t Hsize Hall => [| s0 s IHs] /= t. + rewrite subn0 size_map => _ _. rewrite (_ : map _ _ = map (shiftn sh) t); last by elim: t => //= r t ->. elim: t => [// | t0 t IHt] /=. rewrite to_word_cons filter_cat IHt cat0s {t IHt}. by rewrite filter_gt_shiftn. + case: t => [// | t0 t] /=. rewrite ltnS to_word_cons all_cat => {}/IHs Hrec /andP[{}/Hrec Hrec]. rewrite to_word_cons !filter_cat subSS {}Hrec => /all_filterP ->. suff -> : [seq x <- [seq sh + i | i <- t0] | gtn sh x] = [::]. by rewrite cats0. by rewrite filter_gt_shiftn. - elim: s t Hsize Hall => [| s0 s IHs] /= t. + rewrite subn0 size_map => _ _. elim: t => [// | t0 t IHt] /=. rewrite !to_word_cons !filter_cat map_cat {}IHt. by rewrite filter_le_shiftn. + case: t => [// | t0 t] /=. rewrite ltnS to_word_cons all_cat => {}/IHs Hrec /andP[{}/Hrec Hrec]. rewrite !to_word_cons !filter_cat !map_cat subSS {}Hrec. rewrite filter_le_shiftn => Hall. suff -> : [seq x - sh | x <- s0 & sh <= x] = [::] by rewrite cat0s. elim: s0 Hall {t s t0} => [// | l0 s IHs] /= /andP[H /IHs]. by rewrite leqNgt H. 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