proposition: Lemma Greene_row_leq_plact1 u v1 w v2 k : v2 \in plact1 v1 -> Greene_row (u ++ v1 ++ w) k <= Greene_row (u ++ v2 ++ w) k.
proof: Proof. Proof using. rewrite plact1dual => /Greene_row_leq_plact2 H. rewrite [Greene_row (_ ++ v1 ++ _) k]Greene_row_dual. rewrite [Greene_row (_ ++ v2 ++ _) k]Greene_row_dual. move/(_ (revdual w) (revdual u) k): H. by rewrite /revdual -!rev_cat -!catA. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene