proposition: Lemma trivIset_coverU1 : trivIset P -> [disjoint S & cover P] -> trivIset (S |: P).
proof: Proof. Proof using. move=> Htriv Hdis; case (set_0Vmem S) => [-> | [s Hs]]. - case (boolP (set0 \in P)); first by rewrite setU1E => /eqP ->. apply (@trivIsetU1 _ set0 P) => //= T _. by rewrite -setI_eq0 set0I. - have HS : S \notin P. move: Hdis; rewrite -setI_eq0; apply: contraLR => /negbNE HS. have {}Hs : s \in S :&: cover P. by rewrite in_setI Hs /= /cover; apply/bigcupP; exists S. by apply/eqP/setP => H; have := H s; rewrite Hs in_set0. move: Htriv; rewrite /trivIset big_setU1 //=. + move/eqP ->; rewrite {2}/cover big_setU1 //=. rewrite cardsU; move: Hdis; rewrite -setI_eq0 => /eqP ->. by rewrite cards0 subn0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene