proposition: Lemma trivIset_mem (T : finType) (P : {set {set T}}) x : trivIset P -> #|[set B in P | x \in B]| = (x \in cover P).
proof: Proof. move=> trivP; have [x_covP /=|xNcovP] := boolP (x \in cover P); last first. apply: eq_card0 => B; rewrite !inE. apply: contraNF xNcovP => /andP[BP xB]. by apply/bigcupP; exists B. apply: (@eq_card1 _ (pblock P x)) => B; rewrite !inE. apply/andP/eqP => [[BP xB]|->]; last by rewrite mem_pblock pblock_mem. by apply/setP => y; rewrite (def_pblock _ _ xB). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)