Simple axiomatization of finite map images (also called codomains). This is strongly inspired by the implementation of dom.
It doesn't contain nearly as much lemmas though, mainly because results on the image are generally much weaker than those on the domain, so just using the definition seems simple then providing overly complex lemmas.
Disclaimers: I'm not exactly an expert in Coq but eager to learn more. If you find that my coding style and proofs are ugly, inefficient, impractical or not in keeping with recommended guidelines feel free to let me know.