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