proposition: Lemma size_RSmap2 w : size ((RSmap w).2) = size w.
proof: Proof. Proof using. elim/last_ind: w => [// | w wn]. rewrite /RSmap rev_rcons /=. case: (RSmap_rev (rev w)) => [t rows] /=. case: (instabnrow t wn) => [tr nrow] /= ->. by rewrite size_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab