Add lemma `map_subseteq_inv`.

As pointed out by @swils in https://mattermost.mpi-sws.org/iris/pl/wzsucg5swtrttqhsawdd8pzama this lemma is missing

It's all the way down the file since I need properties of ∖. If someone knows a (short) proof without, we can move the property up, closer towards other properties on the order.

Alternatively we could leave a comment at the place where the proof 'should be', to make it easier to find for people that are browsing the file.

Other than that, LGTM.

changed the description

mentioned in commit 9765b5fe

merged

Merged!