proposition: Lemma eq_inv_is_skew_tableau_reshape_size inner outer (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) (u1 : seq T1) (u2 : seq T2) : size inner = size outer -> eq_inv u1 u2 -> size u1 = sumn (outer / inner) -> is_skew_tableau inner (skew_reshape inner outer u1) -> is_skew_tableau inner (skew_reshape inner outer u2).
proof: Proof. rewrite /skew_reshape. elim: inner outer u1 u2 => [| inn0 inn IHinn] /=; first by case. case=> //= out0 out u1 u2 /eqP. move out0 after inn0; move out after inn. set shres := out / inn. rewrite eqSS => /eqP Hsz Hinv Hszeq /=. have Hszres : sumn shres <= size u1 by rewrite Hszeq; apply leq_addl. have:= Hinv => /eq_invP[Hszu _]; move Hszu after Hinv. set r1 := take (sumn shres) u1; set r2 := take (sumn shres) u2. have Hinvr : eq_inv r1 r2. move: Hinv; rewrite -{1}(cat_take_drop (sumn shres) u1) -{1}(cat_take_drop (sumn shres) u2). by move/eq_inv_catl; apply; rewrite !size_take -Hszu. have Hszr1 : size r1 = sumn shres by rewrite size_takel // Hszres. have {IHinn Hsz Hinvr Hszr1} IH := IHinn _ r1 r2 Hsz Hinvr Hszr1. rewrite !rev_cons !reshape_rcons; first last. - by rewrite sumn_rev addnC Hszeq. - by rewrite -Hszu sumn_rev addnC Hszeq. rewrite sumn_rev !rev_rcons /= !size_drop. move/and4P => [Hnnil /= Hrow Hdom {}/IH -> {r1 r2}]. rewrite -Hszu Hnnil andbT /=. set r1 := drop (sumn shres) u1; set r2 := drop (sumn shres) u2. have /eq_inv_is_row -> //= : eq_inv r1 r2. move: Hinv; rewrite -{1}(cat_take_drop (sumn shres) u1) -{1}(cat_take_drop (sumn shres) u2). by move/eq_inv_catr; apply; rewrite !size_take -Hszu. rewrite {r1}/r2. move: Hdom; case/lastP Hd : (rev (out / inn)) => [// | d dl] /=. have Hsumn : sumn d + dl = sumn shres. rewrite -(sumn_rev (_ / _)) Hd. by rewrite -(sumn_rev (rcons _ _)) rev_rcons /= sumn_rev addnC. rewrite !reshape_rcons ?size_takel // -?Hszu ?Hszres // !rev_rcons /=. apply: eq_inv_skew_dominate; last by rewrite !size_drop !size_take Hszu. have {Hsumn} Hsum : sumn d <= sumn shres by rewrite -Hsumn; apply leq_addr. have HH n m u : n <= m -> m <= size u -> drop n (take m u) ++ (drop m u) = drop n u. move=> Hnm Hu; have := erefl (drop n u). rewrite -{1}(cat_take_drop m u) drop_cat size_takel //. move: Hnm; rewrite leq_eqVlt => /orP[/eqP -> _| -> //]. by rewrite drop_oversize ?cat0s // size_takel //. rewrite HH // HH -?Hszu //. apply (eq_inv_catr (u1 := take (sumn d) u1) (u2 := take (sumn d) u2) ). - by rewrite !cat_take_drop. - by rewrite !size_take -Hszu. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab