proposition: Lemma imsetP D y : reflect (exists2 x, in_mem x D & y = f x) (y \in imset f D).
proof: Proof. by rewrite [@imset]unlock inE; apply: imageP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)