proposition: Lemma trivIset_set_set_co_occ a : trivIset (set_set_co_occ a).
proof: Proof. apply/trivIsetP => S1 S2; case/imsetP => P1 _ HP1; case/imsetP => P2 _ HP2 HP12. subst S1 S2. rewrite /disjoint. apply/pred0P => m /=. apply/negP/negP. rewrite 2!in_set. move: m. apply/forallP; rewrite -negb_exists; apply/negP; case/existsP => i /andP [/andP [_ /eqP H1] /andP [_ /eqP H2]]; contradict HP12. apply/negP/negPn/eqP; by rewrite -H1 -H2. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2