proposition: Lemma is_skew_reshape_tableauP (w : seq nat) : size w = sumn (P / P1) -> reflect (exists tab, [/\ is_skew_tableau P1 tab, shape tab = P / P1 & to_word tab = w]) (is_skew_reshape_tableau P P1 w).
proof: Proof. Proof using Hincl. rewrite /is_skew_reshape_tableau => Hsize; apply (iffP idP). - move=> H; exists (skew_reshape P1 P w); split; first exact H. + exact: (shape_skew_reshape Hincl Hsize). + exact: (to_word_skew_reshape Hincl Hsize). - move=> [tab] [Htab Hsh <-]. rewrite -(diff_shapeK Hincl) -Hsh. rewrite skew_reshapeK; first exact Htab. rewrite -(size_map size) -/(shape tab) Hsh size_diff_shape. exact: size_included. 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