proposition: Lemma subset_leq_card A B : A \subset B -> #|A| <= #|B|.
proof: Proof. move=> sAB. rewrite -(cardID A B) [#|predI _ _|](@eq_card _ A) ?leq_addr //= => x. by rewrite !inE andbC; case Ax: (x \in A) => //; apply: subsetP Ax. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)