proposition: Theorem RSmap_spec w : is_RSpair (RSmap w).
proof: Proof. Proof using. rewrite /is_RSpair. case H : (RSmap w) => [P Q]; apply/and3P; repeat split. - by have:= is_tableau_RSmap1 w; rewrite H. - by have:= is_yam_RSmap2 w; rewrite H. - by have:= shape_RSmap_eq w; rewrite H => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab