proposition: Lemma size_cover_Q : #|cover P| == #|cover Q|.
proof: Proof. Proof using. rewrite -Swap.swap_size_cover. rewrite /Q /swap_set imset_comp. apply/eqP; apply: size_cover_inj. exact: cast_ord_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene