proposition: Lemma RSstdE (p : seq nat) : is_stdtab (RS p) = is_std p.
proof: Proof. rewrite /is_stdtab is_tableau_RS /=. by apply/idP/idP => Hstd; apply: (perm_std Hstd); last rewrite perm_sym; apply: perm_RS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab