proposition: Lemma size_coverI (S : {set {set T}}) B : trivIset S -> \sum_(i in S) #|i :&: B| = #|cover S :&: B|.
proof: Proof. Proof using. move=> /trivIsetP Htriv. have : trivIset [set i :&: B | i in S]. apply/trivIsetP => U1 V1 /imsetP[U HU ->{U1}] /imsetP[V HV ->{V1}] Hneq. rewrite -setI_eq0 setIACA setIid. have : U != V by move: Hneq; apply: contra => /eqP ->. move/(Htriv _ _ HU HV); rewrite -setI_eq0 => /eqP ->. by rewrite set0I. rewrite /trivIset. pose F := (fun S => S :&: B). have -> : cover [set F i | i in S] = F (cover S). rewrite cover_imset /cover. apply: esym; apply: big_morph; last by rewrite /F set0I. by move=> i j /=; rewrite /F setIUl. rewrite {}/F /= => /eqP <-. apply: esym. rewrite (bigID (fun S => S :&: B == set0)) /=. rewrite big1 ?add0n; first last. move=> i /andP[/imsetP[j _ ->{i}]]. by rewrite -setIA setIid => /eqP ->; rewrite cards0. rewrite (eq_bigl (mem ([set i :&: B | i in S & i :&: B != set0]))); first last. move=> i /=; apply/andP/imsetP => [[/imsetP[j Hj ->{i}]] | [/= j]]. - rewrite -setIA setIid => Hint; exists j => //=. by rewrite inE Hj Hint. - rewrite inE => /andP[Hj Hint] ->{i}. split; last by rewrite -setIA setIid Hint. by apply/imsetP; exists j. rewrite big_imset /=; first last. move=> i j /=; rewrite !inE => /andP[HiS HiB] /andP[HjS HjB] /eqP H. apply/eqP; move: H; apply: contraLR => H. move/(_ _ _ HiS HjS H): Htriv. rewrite -setI_eq0 => /eqP; rewrite -setP => Hneq. move: HiB => /set0Pn[x]; rewrite inE => /andP[Hx HxB]. move/(_ x): Hneq; rewrite !inE Hx /= => Hxj. by apply/eqP/setP => /(_ x); rewrite !inE Hx Hxj HxB. apply: esym; rewrite (bigID (fun S => S :&: B == set0)) /=. rewrite big1 ?add0n; last by move=> i /andP[_ /eqP ->]; rewrite cards0. by apply: eq_bigl => i /=; rewrite inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast