proposition: Lemma size_instab t l : is_tableau t -> size_tab (instab t l) = (size_tab t).+1.
proof: Proof. Proof using. rewrite /size_tab -instabnrowE => /(shape_instabnrow l). case (instabnrow t l) => [tr row] /= -> {tr l}. by rewrite sumn_incr_nth. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab