proposition: Lemma Greene_std u k : Greene_row (std u) k = Greene_row u k.
proof: Proof. Proof using. apply/eqP; rewrite eqn_leq; apply/andP; split; apply: leq_Greene. + exact: ksupp_inj_stdI. + exact: ksupp_inj_std. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv