proposition: Lemma card_in_image A : {in A &, injective f} -> #|image f A| = #|A|.
proof: Proof. move=> injf; rewrite (cardE A) -(size_map f); apply/card_uniqP. by rewrite map_inj_in_uniq ?enum_uniq // => x y; rewrite !mem_enum; apply: injf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)