proposition: Lemma cover_set_set_co_occ a : cover (set_set_co_occ a) = set_occ a ta.
proof: Proof. apply/setP => i. rewrite cover_imset. apply/bigcupP. case : ifP; last by move=> /negP H1 H ; move: H1; apply/negP; case H => {H} y0 ; rewrite 3!in_set => _ /andP []. rewrite in_set => /eqP Hi. exists (tb!_i) ; last by rewrite in_set Hi eqxx andTb. rewrite in_set; apply/andP; split => //. apply/existsP; exists i; by rewrite in_set Hi eqxx andTb. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2