proposition: Lemma mapP s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s).
proof: Proof. elim: s => [|x s IHs]; [by right; case|rewrite /= inE]. exact: equivP (orPP eqP IHs) (iff_sym exists_cons). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)