proposition: Lemma trivIset_disjoint i : i \in x -> i \notin cover C -> trivIset (x |: C) -> [disjoint x & cover C].
proof: Proof. move=> Hpx Hp Hxc. rewrite disjoints_subset. apply/subsetP => j Hjx. rewrite inE. apply/negP => /bigcupP [y Hy Hiy]. move/trivIsetP/(_ x y): Hxc. rewrite !inE eqxx Hy /= orbT. case: eqP => Hxy. - subst y. move/bigcupP: Hp; elim. by exists x. - move/(_ erefl erefl erefl). by rewrite (disjoint_I_false Hjx). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist