proposition: Lemma trivIset_setrev P : trivIset P = trivIset (rev_ksupp P).
proof: Proof. Proof using. apply/idP/idP. - by apply: imset_trivIset; exact rev_ord_cast_inj. - by rewrite -{2}(rev_ksuppK P); apply: preimset_trivIset. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene