proposition: Lemma trivIseq_cover S : trivIseq S -> \sum_(i <- S) #|i| = #|\bigcup_(i <- S) i|.
proof: Proof. Proof using. elim: S => [_ | s0 s IHs] /=; first by rewrite !big_nil cards0. move=> Htriv; move/(_ (trivIseq_consK Htriv)): IHs => IHs. move: Htriv; rewrite !big_cons /trivIseq => Htriv. rewrite cardsU -IHs. suff -> : #|s0 :&: \big[setU (T:=T)/set0]_(j <- s) j| = 0 by rewrite subn0. apply/eqP; rewrite cards_eq0; apply/eqP/setP => i. rewrite !inE; apply/negP => /andP[Hi]. rewrite bigcup_seq => /bigcupP[X HX HiX]. have:= HX; rewrite -!index_mem => Hind. have: 0 < (index X s).+1 < size (s0 :: s) by rewrite /= ltnS Hind. move/Htriv => /=; rewrite (nth_index set0 HX). move/disjoint_setI0; apply/setP => /(_ i). by rewrite !inE Hi HiX. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast