Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming

!507 (closed) ballooned into this huge change. This contains the following two MRs:

• !526 (merged)
• !531 (merged)

There is more that could be done, but that is postponed (we should probably open an issue):

• non_empty change as discussed in !526 (comment 97794)
• Direction of equality in fmap/omap/alter lemmas, see !531 (comment 97789)

stdpp/fin_maps.v

@@ -3761,7 +3761,7 @@ Section map_seq.
   Proof.
     intros. apply map_eq. intros j. destruct (decide (i = j)) as [->|?].
     - rewrite lookup_insert_eq, lookup_map_seq, option_guard_True by lia.
-      by rewrite list_lookup_insert by lia.
+      by rewrite list_lookup_insert_eq by lia.
     - rewrite lookup_insert_ne, !lookup_map_seq by done.
       case_guard; [|done]. by rewrite list_lookup_insert_ne by lia.
   Qed.
@@ -3892,7 +3892,7 @@ Section map_seqZ.
   Proof.
     intros. apply map_eq. intros j. destruct (decide (i = j)) as [->|?].
     - rewrite lookup_insert_eq, lookup_map_seqZ, option_guard_True by lia.
-      by rewrite list_lookup_insert by lia.
+      by rewrite list_lookup_insert_eq by lia.
     - rewrite lookup_insert_ne, !lookup_map_seqZ by done.
       case_guard; [|done]. by rewrite list_lookup_insert_ne by lia.
   Qed.