proposition: Lemma shape_invseq s t : invseq s t -> shape (RS s) = shape (RS t).
proof: Proof. move=> Hinv; apply: Greene_row_tab_eq_shape; try apply: is_tableau_RS. move=> k; rewrite -!(Greene_row_invar_plactic (congr_RS _) k). exact: Greene_invseq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv