proposition: Lemma swap_cover (P : {set {set 'I_(size x)}}) : cover (swap_set @: P) = swap_set (cover P).
proof: Proof. Proof using. rewrite cover_imset /cover; apply: esym; apply: big_morph. - move=> i j /=; exact: imsetU. - exact: imset0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene