proposition: Lemma disjointU1 x A B : [disjoint predU1 x A & B] = (x \notin B) && [disjoint A & B].
proof: Proof. by rewrite disjointU disjoint1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)