proposition: Lemma disjoint_subset A B : [disjoint A & B] = (A \subset [predC B]).
proof: Proof. by rewrite subset_disjoint; apply: eq_disjoint_r => x; rewrite !inE /= negbK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)