proposition: Lemma shape_instabnrow t l : is_tableau t -> let: (tr, nrow) := instabnrow t l in shape tr = incr_nth (shape t) nrow.
proof: Proof. Proof using. case H : (instabnrow t l) => [tr nrow] Htab. elim: t Htab l tr nrow H => [/= _| t0 t IHt /= /and4P[_ Hrow _ Htab]] l tr nrow /=; first by move=> [<- <-]. case (boolP (bump t0 l)) => [Hbump | Hnbump]. - rewrite (bump_bumprowE Hrow Hbump). case: nrow => [|nrow]; first by case (instabnrow t (bumped t0 l)). case Hins: (instabnrow t (bumped t0 l)) => [tres nres] [] <- <- /=. move/(_ Htab (bumped t0 l) tres nres Hins): IHt => ->. by rewrite (bump_size_ins Hrow Hbump). - have:= nbump_bumprowE Hrow Hnbump => -> [] <- <- /=. by rewrite (nbump_size_ins Hrow Hnbump). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab