proposition: Lemma subset_disjoint A B : (A \subset B) = [disjoint A & [predC B]].
proof: Proof. by rewrite disjoint_sym unlock. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)