Add set_omap to finite sets

Add omap-like function to finite sets, aka OCaml's filter_map operation.

I needed it to destruct a set of X + Y into a set of X and a set of Y.

Also add a few lemmas to reason about it.

CHANGELOG.md

@@ -25,6 +25,8 @@ Coq 8.12 and 8.13 are no longer supported by this release.
 - Add `by` parameter to `multiset_solver`, which defaults to `eauto`.
 - Add `map_img` operator for map image/codomain and some lemmas about it. (by
   Dorian Lesbre)
+- Add `set_omap` function for finite sets and associated lemmas.
+
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).