proposition: Lemma Greene_col_invar_plact1 u v1 w v2 k : v2 \in plact1 v1 -> Greene_col (u ++ v1 ++ w) k = Greene_col (u ++ v2 ++ w) k.
proof: Proof. Proof using. move=> H; apply/eqP; rewrite eqn_leq; apply/andP; split. - exact: Greene_col_leq_plact1. - by apply: Greene_col_leq_plact1i; rewrite -plact1I. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene