proposition: Lemma subsetPn A B : reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)).
proof: Proof. rewrite unlock; apply: (iffP (pred0Pn _)) => [[x] | [x Ax nBx]]. by case/andP; exists x. by exists x; rewrite /= nBx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)