Two reasons:

- The equality makes it very hard to use the lemma with `rewrite`.
- The version for lists `insert_zip_with` does not have the equality either.

Add link to docs to the Readme

See merge request iris/stdpp!42

Explicitly use core hint database

See merge request iris/stdpp!43

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

- Interaction with delete
- Make name about map interacting with insert consistent.

MR #41 relies on https://github.com/coq/coq/issues/5039, which has
not been fixed in Coq 8.6.

Consistently block `simpl` on all `Z` operations

See merge request iris/stdpp!41

This makes some proress on #21. Still, the question remains if a more
generic solution exists.

TIMED is still supported