proposition: Lemma Greene_row_dual : Greene_row w k = Greene_row (revdual w) k.
proof: Proof. Proof using. rewrite /Greene_col. apply/eqP; rewrite eqn_leq; apply/andP; split. - apply: leq_Greene; rewrite /ksupp_inj => S HS; exists (rev_ksupp S). rewrite size_cover_rev eq_refl /=. by rewrite rev_is_ksupp_row in HS. - apply: leq_Greene; rewrite /ksupp_inj => S HS. exists (rev_ksupp_inv S); rewrite -{1}[S]rev_ksuppKV size_cover_rev eq_refl /=. by move: HS; rewrite -{1}[S]rev_ksuppKV rev_is_ksupp_row. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene