proposition: Corollary Greene_col_leq_plact2i : v2 \in plact2i v1 -> Greene_col (u ++ v1 ++ w) k <= Greene_col (u ++ v2 ++ w) k.
proof: Proof. Proof using. by move /ksuppCol_inj_plact2i; apply: leq_Greene. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene