proposition: Lemma size_cover_bnotin : #|cover P| == #|cover Qbnotin|.
proof: Proof. Proof using. by rewrite Swap.swap_size_cover. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene