proposition: Theorem size_RS w : size_tab (RS w) = size w.
proof: Proof. Proof using. elim/last_ind: w => [// | w0 w]. rewrite /RS rev_rcons /= -[(RS_rev (rev w0))]/(RS w0). by rewrite (size_instab _ (is_tableau_RS _)) size_rcons => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab