proposition: Lemma shape_bijLR yam : yam \in LRyam_set -> shape (bijLR yam) = P.
proof: Proof. Proof using . rewrite !inE /bijLR /= => Hskew. case (boolP (is_skew_reshape_tableau P P1 yam)) => [_|] /=; last by rewrite Hskew. rewrite /shape /join_tab. rewrite !size_map -map_comp. rewrite (eq_map (g := fun p => size p.1 + size p.2)); first last. by move=> i /=; rewrite size_cat. rewrite size_zip2 size_skew_reshape. rewrite (_ : map size _ = pad 0 (size P) P1); first last. rewrite /pad /= map_cat. rewrite -(size_map size) -/(shape (RS _)) shape_RS_std. rewrite shape_RS_yam; last by apply hyper_yamP; apply intpartnP. rewrite (evalseq_hyper_yam (intpartnP P1)). by rewrite map_nseq. rewrite (_ : map size _ = P / P1); first last. rewrite /= -map_comp. rewrite (eq_map (g := size)); last by move=> i /=; rewrite size_map. rewrite -/(shape _) shape_skew_reshape //=. by rewrite size_std size_yameval sumn_diff_shape_intpartE. rewrite -(size_diff_shape P1 P). rewrite -/(outer_shape P1 (P / P1)). exact: diff_shapeK. 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