proposition: Lemma trivIsetS_f (A B : finType) (f : A -> B) (AA : {set {set A}}) (BB : {set {set B}}) : (forall a, a \in AA -> exists b, b \in BB /\ a = [set a' | f a' \in b]) -> trivIset BB -> trivIset AA.
proof: Proof. move=> /= Hsub. move/trivIsetP => Hdisj. apply/trivIsetP => /= x y Hx Hy. rewrite -setI_eq0. case: (Hsub _ Hx) => x' [] x'Q ->. case: (Hsub _ Hy) => y' [] y'Q -> xy. have {xy} : x' != y' by apply: contra xy => /eqP ?; subst y'. move/(Hdisj _ _ x'Q y'Q). rewrite -setI_eq0 => /eqP abs. apply/eqP/setP => /= m0. rewrite in_set0. move/setP : abs => /(_ (f m0)). rewrite in_set0 => /negbT. rewrite inE negb_and !inE. case/orP; move/negbTE => -> //; by rewrite andbF. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2