Add `gmultiset_map` and associated lemmas

This merge request adds a definition for mapping over a gmultiset, gmultiset_map, similar to set_map for (regular) finite sets.

I struggled with finding a correct location for the definition and associated lemmas in gmultiset.v. I am open to any suggestions to improve the placement.