proposition: Lemma trivIset_coverD1 : trivIset P -> S \in P -> [disjoint S & cover (P :\ S)].
proof: Proof. Proof using. move=> /trivIsetP Htriv HS; rewrite /cover bigcup_disjoint //=. move=> T; rewrite inE in_set1 eq_sym => /andP[Hneq HT]. exact: Htriv. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene