proposition: Theorem invinstabnrowK t l : is_tableau t -> invinstabnrow (instab t l) (instabnrow t l).2 = (t, l).
proof: Proof. Proof using. elim: t l => [l // | t0 t IHt] l /= /and4P[Hnnil Hrow0 Hdom Htab]. case (boolP (bump t0 l)) => [Hbump | Hnbump]. - rewrite (bump_bumprowE Hrow0 Hbump) /=. move/(_ (bumped t0 l) Htab): IHt. case Hres : (instabnrow t (bumped t0 l)) => [tres nres] /= ->. by rewrite (invbumprowK Hrow0 Hbump). - rewrite (nbump_bumprowE Hrow0 Hnbump) (nbump_ins_rconsE Hrow0 Hnbump) /=. case Hres : (rcons t0 l) => [| ares tres]; first by move: Hres; case t0. case eqP => Htres. exfalso; move: Hnnil; have:= eq_refl (size (rcons t0 l)). by rewrite {2}Hres Htres size_rcons /= => /nilP ->. congr (_ :: _ , _). by move: Hres => /(congr1 (belast l)); rewrite belast_rcons => [][->]. by move: Hres => /(congr1 (last l)); rewrite last_rcons => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab