proposition: Theorem instabnrowinvK t nrow : is_tableau t -> t != [::] -> is_rem_corner (shape t) nrow -> let: (tin, l) := invinstabnrow t nrow in (instabnrow tin l) = (t, nrow).
proof: Proof. Proof using. elim: t nrow => [// | t0 t IHt] nrow /= /and4P[Hnnil0 Hrow0 Hdom Htab _]. rewrite /is_rem_corner. case: nrow => [{IHt} /= Hcorn | nrow Hcorn]. + case: t0 Hnnil0 Hrow0 Hdom Hcorn => [// | l0 t0 _]. case eqP => [/= -> _ _ | Hnnil0 Hrow0 _ _]. * case: t Htab => [// | t1 t] /= /and4P[Ht _ _ _ Hsz]. by exfalso; move: Ht Hsz; case t1. * elim/last_ind: t0 Hnnil0 Hrow0 => [// | tt0 ln IHtt0] _ Hrow0. have:= head_leq_last_row Hrow0. rewrite belast_rcons last_rcons /= leNgt => /negbTE ->. move: Hrow0 => /= /is_row_cons[_ Hrow0]. by rewrite (bumprow_rcons Hrow0). + have Hnnil : (t != [::]) by move: Hcorn; case t => //=; rewrite nth_nil. move/(_ nrow Htab Hnnil Hcorn): IHt => {Hcorn} /=. case H: (invinstabnrow t nrow) => [tin l]. have Hinvbump: (invbump l t0) by apply: (@invbump_dom t0 t tin l nrow). have:= bumprowinvK Hnnil0 Hrow0 Hinvbump. rewrite /invins /invbumped. by case (invbumprow l t0) => [t0r l0r] /= -> ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab