proposition: Lemma imset_injP : reflect {in D &, injective f} (#|f @: D| == #|D|).
proof: Proof. by rewrite [@imset]unlock cardsE; apply: image_injP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)