proposition: Corollary Greene_col_eq_shape_RS (d1 d2 : unit) (S : inhOrderType d1) (T : inhOrderType d2) (s : seq S) (t : seq T) : (forall k, Greene_col s k = Greene_col t k) -> (shape (RS s) = shape (RS t)).
proof: Proof. move=> HGreene; apply: Greene_col_tab_eq_shape; try apply: is_tableau_RS. move=> k. rewrite -(Greene_col_invar_plactic (u := s)); last exact: congr_RS. rewrite -(Greene_col_invar_plactic (u := t)); last exact: congr_RS. exact: HGreene. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene