proposition: Theorem is_tableau_RS w : is_tableau (RS w).
proof: Proof. Proof using. elim/last_ind: w => [// | w l0] /=. rewrite /RS rev_rcons /=. exact: is_tableau_instab. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab