proposition: Lemma RSclassP tab : is_tableau tab -> all (fun w => RS w == tab) (RSclass tab).
proof: Proof. Proof using. move=> Htab /=; apply/allP => w /mapP[Q]. move /(allP (enum_yamevalP (is_part_sht Htab))). rewrite /is_yam_of_eval => /andP[Hyam /eqP Hsh] ->{w}. by rewrite -RSmapE RSmapinv2K //= Htab Hyam Hsh /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab