proposition: Lemma disjointU A B C : [disjoint predU A B & C] = [disjoint A & C] && [disjoint B & C].
proof: Proof. case: [disjoint A & C] / (pred0P (xpredI A C)) => [A0 | nA0] /=. by congr (_ == 0); apply: eq_card => x; rewrite [x \in _]andb_orl A0. apply/pred0P=> nABC; case: nA0 => x; apply/idPn=> /=; move/(_ x): nABC. by rewrite [_ x]andb_orl; case/norP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)