proposition: Lemma subset_cardP A B : #|A| = #|B| -> reflect (A =i B) (A \subset B).
proof: Proof. move=> 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 choice) mathcomp(path div)