proposition: Lemma is_rem_corner_instabnrow t l : is_tableau t -> let: (res, nrow) := instabnrow t l in is_rem_corner (shape res) nrow.
proof: Proof. Proof using. rewrite /is_rem_corner. elim: t l => [l _ | t0 t IHt l /and4P[Hnnil Hrow /dominateP[Hdom _] Htab]] //=. case (boolP (bump t0 l)) => [Hbump | Hnbump]. - rewrite (bump_bumprowE Hrow Hbump) /=. move/(_ (bumped t0 l) Htab): IHt. by case (instabnrow t (bumped t0 l)) => [res nrow]. - rewrite (nbump_bumprowE Hrow Hnbump) (nbump_ins_rconsE Hrow Hnbump) /= size_rcons. by move: Hdom; rewrite -nth0 /=; case t. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab