proposition: Lemma imset_proper (A B : {set aT}) : {in B &, injective f} -> A \proper B -> f @: A \proper f @: B.
proof: Proof. move=> injf /properP[sAB [x Bx nAx]]; rewrite properE imsetS //=. apply: contra nAx => sfBA. have: f x \in f @: A by rewrite (subsetP sfBA) ?imset_f. by case/imsetP=> y Ay /injf-> //; apply: subsetP sAB y Ay. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)