proposition: Lemma shape_RSmap_eq w : shape (RSmap w).1 = evalseq (RSmap w).2.
proof: Proof. Proof using. elim/last_ind: w => [// | w l0]; rewrite /RSmap rev_rcons /=. have:= is_tableau_RSmap1 w; rewrite /RSmap. case: (RSmap_rev (rev w)) => [t rows] /= Htab. have:= shape_instabnrow l0 Htab. case: (instabnrow t l0) => [tr row]. by rewrite /= => -> ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab