proposition: Lemma disjoint_I_false p (x x' : {set T}) : p \in x -> p \in x' -> [disjoint x & x'] = false.
proof: Proof. move=> Hpx Hpx'; rewrite disjoints_subset. apply/subsetP => /(_ p Hpx). by rewrite inE Hpx'. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist