proposition: Lemma disjointsU1 (T: finType) (A B: {set T}) x: [disjoint (x |: A) & B] = (x \notin B) && [disjoint A & B].
proof: Proof. rewrite - !setI_eq0 setIUl; case h: (x \in B) => /=. by apply /set0Pn; exists x; rewrite !inE h eqxx. rewrite (_ : [set x] :&: B = set0) ? set0U //. by apply /setP => y; rewrite !inE; apply /andP => [[/eqP ->]]; rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)