Generalize `map_filter_insert` so that it covers both the True and False case.

The new lemma is

Lemma map_filter_insert m i x :
  filter P (<[i:=x]> m)
  = if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).

We need the delete because there might be another entry with key i in m.

In addition there are the lemmas:

Lemma map_filter_insert_True m i x : (* used to be map_filter_insert *)
  P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
Lemma map_filter_insert_False m i x : (* used to be map_filter_insert_not_delete *)
  ¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).

I use the _True and _False suffixes similar to decide_True and decide_False.

See discussion in !245 (335bc4d6, comment 72118) for the discussion that led to this MR.

CHANGELOG.md

@@ -141,6 +141,9 @@ API-breaking change is listed.
   + Remove `map_to_list_empty_inv_alt`; chain `Permutation_nil_r` and
     `map_to_list_empty_iff` instead.
   + Add lemma `map_filter_empty_iff`.
+- Generalize `map_filter_insert` so that it covers both the True and False case.
+  Use `_True` and `_False` for the specific cases. Weaken premise of
+  `map_filter_delete_False` to make it consistent with `map_filter_insert_False'`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -195,6 +198,11 @@ s/\bsize_empty_inv\b/size_empty_iff/g
 s/\bdom_empty_inv(_L|)\b/dom_empty_iff\1/g
 s/\bgmultiset_elements_empty('|_inv)\b/gmultiset_elements_empty_iff/g
 s/\bgmultiset_size_empty_inv\b/gmultiset_size_empty_iff/g
+# map_filter_insert
+s/\bmap_filter_insert\b/map_filter_insert_True/g
+s/\bmap_filter_insert_not('|)\b/bmap_filter_insert_False\1/g
+s/\bmap_filter_insert_not_delete\b/map_filter_insert_delete_False/g
+s/\bmap_filter_delete_not\b/map_filter_delete_False/g
 EOF
 ```