proposition: Lemma trivIset_I1 i : trivIset (x |: C) -> i \in x -> i \in cover C -> x \in C.
proof: Proof. move=> Htriv Hix /bigcupP [y Hy Hiy]. move/trivIsetP/(_ x y): Htriv. rewrite !inE eqxx Hy orbT /=. case: eqP => [-> //|] _ /=. move/(_ erefl erefl erefl). by rewrite (disjoint_I_false Hix). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist