Add insert delete lemma for big ops over gmap

Merged Simon Friis Vindum requested to merge simonfv/iris:big-op-insert-delete into master

These lemmas are similar to insert_delete but for big ops over gmaps.

They are convenient when one has deleted a conjunc with big_opM_delete and then later wants to add it back in.

Merge request reports