proposition: Lemma hb_strip_rowE inner outer u : is_part inner -> is_part outer -> is_row u -> size u = sumn (outer / inner) -> included inner outer && is_skew_tableau inner (skew_reshape inner outer u) = hb_strip inner outer.
proof: Proof. Proof using. move=> Hpartin Hpartout Hrow Hsize. apply/andP/idP => [[] Hincl /(row_hb_strip Hpartin) | Hstrip]. - rewrite (to_word_skew_reshape Hincl Hsize) => /(_ Hrow). by rewrite (shape_skew_reshape Hincl Hsize) (diff_shapeK Hincl). - split; first exact: hb_strip_included. elim: inner outer Hpartout u Hsize Hrow Hstrip {Hpartin} => [| inn0 inn IHinn] [//= | out0 out]. move=> + u + Hrow /eqP Hout; rewrite {}Hout /=. rewrite addn0 add0n andbT => /[swap] <- /lt0n_neq0 Hn0. by rewrite take_size Hrow eq_refl !andbT. set dsh := out / inn. move=> Hpartout /= u Hsize Hrow /andP[/andP[Hhead0 H0] Hstrip]. rewrite /skew_reshape /= rev_cons reshape_rcons; first last. by rewrite sumn_rev Hsize /= addnC. rewrite rev_rcons -/dsh /=. apply/and4P; split. - rewrite size_drop sumn_rev Hsize /= addnK (subnKC H0). exact: (part_head_non0 Hpartout). - exact: is_row_drop. - apply skew_dominate_no_overlap. rewrite -/(skew_reshape _ _ _) sumn_rev. have : size (take (sumn dsh) u) = sumn dsh. by rewrite size_takel // Hsize leq_addl. move/(shape_skew_reshape (hb_strip_included Hstrip)). set sh := skew_reshape _ _ _ => Hshape. have -> : size (head [::] sh) = head 0 (shape sh). by rewrite /shape; case sh. rewrite Hshape {IHinn Hsize Hrow sh Hshape Hstrip dsh}. case: inn => [| inn1 inn] /=; first by rewrite subn0. case: out Hhead0 {Hpartout} => //= out1 out H. exact: leq_sub2r. - rewrite -/(skew_reshape _ _ _); apply IHinn. + by move: Hpartout => /= /andP[]. + by rewrite sumn_rev size_takel // Hsize leq_addl. + exact: is_row_take. + exact: Hstrip. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab