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/binders.v

@@ -108,5 +108,5 @@ Section binder_delete_insert.
   Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
   Lemma binder_delete_delete {A} b s (m : M A) :
     binder_delete b (delete s m) = delete s (binder_delete b m).
-  Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
+  Proof. destruct b; simpl; by rewrite 1?delete_delete. Qed.
 End binder_delete_insert.