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