fact: Fixpoint RSmap_rev w : (seq (seq T)) * (seq nat) := if w is w0 :: wtl then let: (t, rows) := RSmap_rev wtl in let: (tr, nrow) := instabnrow t w0 in (tr, nrow :: rows) else ([::], [::]).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab