proposition: Lemma tuto_subsetP : forall A B, reflect {subset A <= B} (A \subset B).
proof: Proof. rewrite unlock. move=> A B; apply: (iffP idP). by move/pred0P=> h x Ax; move: (h x)=> /=; rewrite Ax andbT; move/negbFE. by move=> h; apply/pred0P=> x /=; case Ax : (x \in A); rewrite ?andbF // h. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)