proposition: Lemma tuto_subset_cardP : forall A B, #|A| = #|B| -> reflect (A =i B) (A \subset B).
proof: Proof. move=> A B eqcAB; case: (@subsetP _ A B) (@subset_eqP _ A B) => //= sAB. case: (@subsetP _ B A) => [//|[]] x Bx; apply/idPn => Ax. case/idP: (ltnn #|A|); rewrite {2}eqcAB (cardD1 x B) Bx /=. apply: subset_leq_card; apply/subsetP=> y Ay; rewrite inE /= andbC. by rewrite sAB //; apply/eqP => eqyx; rewrite -eqyx Ay in Ax. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)