proposition: Theorem RSmapK w : RSmapinv2 (RSmap w) = w.
proof: Proof. Proof using. rewrite /RSmapinv2. elim/last_ind: w => [// | w wn]; rewrite /RSmap /RS rev_rcons /=. have:= is_tableau_RSmap1 w; rewrite /RSmap. case Hbij : (RSmap_rev (rev w)) => [t rows] /= Htab IHw. have:= invinstabnrowK wn Htab; rewrite -(instabnrowE t wn). case (instabnrow t wn) => [tr row] /= ->. by rewrite IHw. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab