proposition: Corollary RS_tabE (t : seq (seq Alph)) : is_tableau t -> RS (to_word t) = t.
proof: Proof. Proof using. move=> Htab. have : is_RSpair (t, hyper_yam (shape t)). rewrite /is_RSpair Htab (hyper_yamP (is_part_sht Htab)) /=. by rewrite (evalseq_hyper_yam (is_part_sht Htab)). move/RSmapinv2K; set w := (X in RSmap X); move=> Hw. have:= RSmapE w; rewrite Hw /= => ->. have:= congr_RS w. by rewrite plactic_RS => /eqP <-. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene