proposition: Lemma RStabK : cancel RStab RStabinv.
proof: Proof. Proof using. rewrite /RStab /RStabinv /RStabmap. move=> w /=; have:= is_yam_RSmap2 w. case H : (RSmap w) => [P Q] /= Hyam. by rewrite stdtab_of_yamK; first by rewrite -H (RSmapK w). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab