proposition: Lemma size_rev_ksupp P : #|rev_ksupp P| = #|P|.
proof: Proof. Proof using. by rewrite card_imset; last exact: rev_set_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene