proposition: Lemma disjointFr A B x : [disjoint A & B] -> x \in A -> x \in B = false.
proof: Proof. by move/pred0P/(_ x) => /=; case: (x \in A). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)