proposition: Lemma is_tableau_instabnrowinv1 (s : seq (seq T)) nrow : is_tableau s -> is_rem_corner (shape s) nrow -> is_tableau (invinstabnrow s nrow).1.
proof: Proof. Proof using. rewrite /is_rem_corner. elim: s nrow => [/= |s0 s IHs] nrow; first by case nrow. case: nrow => [/= | nrow]. - move=> {IHs} /and4P[]; case: s0 => [// | s0h s0t] _. case eqP => [-> /= _ _ | /eqP Hnnil]; first by case s. case/lastP: s0t Hnnil => [// | s0t s0l] _; rewrite -!rcons_cons => Hrow. rewrite belast_rcons. case Ht : s => [/= | s1 s']; first by have:= is_row_rconsK Hrow => /= ->. rewrite -Ht /= => Hdom -> Hshape. have:= is_row_rconsK Hrow => /= -> /=; rewrite andbT. rewrite -rcons_cons in Hdom. move: Hdom; rewrite -cats1; apply: dominate_cut. by move: Hshape; rewrite Ht /= size_rcons ltnS. - case Hs : s => [/= | s1 s']; first by rewrite nth_nil. rewrite -Hs => /= /and4P[Hnnil0 Hrows0 Hdom Htabs] Hcorn. have:= Htabs; rewrite {1}Hs; move/head_tableau_non_nil => Hnnil1. move/(_ _ Htabs Hcorn): IHs. have Hnnils : (s != [::]) by rewrite Hs. move/(instabnrowinvK Htabs Hnnils): Hcorn. case Hinv1 : (invinstabnrow s nrow) => [t l0] /= Hins1 Htabt. move: {Hnnils Htabs Hinv1} (invbump_geq_head Hnnils Htabs Hinv1). have:= instabnrowE t l0; rewrite Hins1 /= Hs => {}Hins1. move: Hdom; rewrite {s}Hs /= => Hdom. have:= dominate_head Hnnil1 Hdom. rewrite (set_head_default l0 inh Hnnil0) (set_head_default l0 inh Hnnil1). move=> /lt_le_trans /[apply] /(bumprowinvK Hnnil0 Hrows0). have:= is_row_invins l0 Hrows0; have:= size_invins l0 s0; rewrite /invins /invbumped. case Hinv0: (invbumprow l0 s0) => [t0 l] /= Hsize Hrowt0 Hins0. have Hnnilt0: (t0 != [::]) by move: Hnnil0 Hsize; case t0 => [//=|]; case s0. rewrite Hnnilt0 Hrowt0 Htabt andbT /=. case Ht : t Htabt => [// | t1 t'] /tableau_is_row Hrowt1 /=. have:= @head_instab t1 t' l0 Hrowt1. rewrite -{}Ht -{}Hins1 /= => Hins {t t' s'}. have Hbump : (bump t0 l). case (boolP (bump t0 l)) => [//= | Hnbump]. by have:= nbump_bumprowE Hrowt0 Hnbump; rewrite Hins0. apply: (bump_dominateK Hrowt0 Hrowt1 Hbump). have:= bump_bumprowE Hrowt0 Hbump. by rewrite /bumped Hins0 => [][<- <-]; rewrite -Hins. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab