proposition: Lemma tuto_subsetPn : forall A B, reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)).
proof: Proof. rewrite unlock. move=> A B; apply: (iffP idP). by move/pred0Pn=> [x] /=; case/andP=> nAx Bx; exists x. by case=> x Ax nBx; apply/pred0Pn; exists x; rewrite /= nBx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)