proposition: Lemma codomfP f v : reflect (exists x, f.[? x] = Some v) (v \in codomf f).
proof: Proof. apply: (iffP (imfsetP _ _ _ _)) => /= [[x _ ->]|[k]]. by exists (val x); rewrite Some_fnd. by case: fndP => //= kf [<-]; exists [` kf]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)