Make `union_Some` a `↔`, add `union_None` and `union_is_Some`.

This makes it more consistent with other Some lemmas, that are also bidirectional.

See also the discussion !466 (comment 91517)

The change to union_Some is not backwards compatible, so we need to either provide a new lemma (with a new name, but what?) for the → direction, or we need to update existing code. It's not clear to me how much union_Some is used in reverse dependencies.