proposition: Lemma trivIset_coverU : trivIset P -> trivIset Q -> [disjoint cover P & cover Q] -> trivIset (P :|: Q).
proof: Proof. Proof using. move=> /trivIsetP HtrivP /trivIsetP HtrivQ Hdis. apply/trivIsetP => A B; rewrite !inE. move=> /orP[] HA /orP[] HB Hneq. - exact: HtrivP. - exact: disjoint_cover. - by rewrite disjoint_sym; exact: disjoint_cover. - exact: HtrivQ. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene