proposition: Lemma Greene_col_invar_plact1i u v1 w v2 k : v2 \in plact1i v1 -> Greene_col (u ++ v1 ++ w) k = Greene_col (u ++ v2 ++ w) k.
proof: Proof. Proof using. by rewrite -plact1I => H; apply: esym; apply: Greene_col_invar_plact1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene