proposition: Lemma imset_inj : injective f -> injective (fun A : {set aT} => f @: A).
proof: Proof. move=> inj_f A B => /setP E; apply/setP => x. by rewrite -(mem_imset A x inj_f) E mem_imset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)