proposition: Theorem count_RS w p : count p w = count p (to_word (RS w)).
proof: Proof. Proof using. elim/last_ind: w => [// | w0 w]. rewrite /RS !rev_rcons /= -[(RS_rev (rev w0))]/(RS w0). rewrite (count_instab _ _ (is_tableau_RS _)) => <-. by rewrite -[rcons _ _](revK) rev_rcons count_rev /= count_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab