proposition: Lemma image_injP A : reflect {in A &, injective f} (#|image f A| == #|A|).
proof: Proof. apply: (iffP eqP) => [eqfA |]; last exact: card_in_image. by apply/dinjectiveP; apply/card_uniqP; rewrite size_map -cardE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)