proposition: Lemma bijRS : bijective RSbij.
proof: Proof. Proof using. split with (g := RSbijinv); rewrite /RSbij /RSbijinv. - by move=> w /=; rewrite (RSmapK w). - by move=> [pq H]; apply: pyampair_inj => /=; exact (RSmapinv2K H). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab