proposition: Corollary plactic_shapeRS_row_proof u v : u =Pl v -> shape (RS u) = shape (RS v).
proof: Proof. Proof using. move=> Hpl. suff HeqRS k : Greene_row (to_word (RS u)) k = Greene_row (to_word (RS v)) k by apply: (Greene_row_tab_eq_shape (is_tableau_RS u) (is_tableau_RS v) HeqRS). rewrite -!(Greene_row_invar_plactic (congr_RS _) k). exact: Greene_row_invar_plactic. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene