proposition: Theorem is_tableau_instab t l : is_tableau t -> is_tableau (instab t l).
proof: Proof. Proof using. elim: t l => [l _ // | t0 t IHt l Htab]. move: Htab => /= /and4P[Ht0 Hrow0 Hdom Htab]. case (boolP (bump t0 l)) => [Hbump0 | Hnbump0]. - rewrite /= (bump_bumprowE Hrow0 Hbump0). case: t IHt Hdom Htab => [_ _ _ | t1 t IHt Hdom Htab] /=. * rewrite ins_non_nil (is_row_ins Hrow0) andbT /=. rewrite -[[:: bumped t0 l]]/(ins [::] ( bumped t0 l)). exact: bump_dominate. * have Hrow1 := tableau_is_row Htab. rewrite (head_instab _ _ Hrow1). move/(_ (bumped t0 l) Htab) : IHt => /= ->. rewrite ins_non_nil (is_row_ins Hrow0) /= andbT. exact: bump_dominate. - rewrite /= (nbump_bumprowE Hrow0 Hnbump0) /= Htab. rewrite ins_non_nil (is_row_ins Hrow0) /= andbT. by rewrite (nbump_ins_rconsE Hrow0 Hnbump0); exact: dominate_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab