proposition: Corollary Greene_row_RS k w : Greene_row w k = sumn (take k (shape (RS w))).
proof: Proof. Proof using. rewrite -Greene_row_tab; last exact: is_tableau_RS. by apply: Greene_row_invar_plactic; exact: congr_RS. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene