proposition: Lemma mem_codomf f v : (v \in codomf f) = [exists x : domf f, f x == v].
proof: Proof. apply: sameP existsP. by apply: (iffP (imfsetP _ _ _ _)) => /= [[x _ ->]|[x /eqP <-]]; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)