proposition: Lemma subset_leqif_card A B : A \subset B -> #|A| <= #|B| ?= iff (B \subset A).
proof: Proof. move=> sAB; split; [exact: subset_leq_card | apply/eqP/idP]. by move/subset_cardP=> sABP; rewrite (eq_subset_r (sABP sAB)). by move=> sBA; apply: eq_card; apply/subset_eqP; rewrite sAB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)