proposition: Lemma disjointsU1 x (A B : {set T}) : [disjoint x |: A & B] = (x \notin B) && [disjoint A & B].
proof: Proof. by rewrite !disjoints_subset subUset sub1set inE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist