proposition: Lemma swap_size_cover (P : {set {set 'I_(size x)}}) : #|cover (swap_set @: P)| = #|cover P|.
proof: Proof. Proof using. by rewrite swap_cover card_imset; last exact swap_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene