proposition: Lemma trivIset_I (S : {set {set T}}) B : trivIset S -> \sum_(i in S) #|i :&: B| <= #|B|.
proof: Proof. Proof using. move/size_coverI ->; apply: subset_leq_card. by apply/subsetP => i; rewrite !inE => /andP[]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast