This is in preparation for coq/coq#9274.

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.

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.

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

Works around Coq bug #7731

The notation was parsing-only and all it did was reorder the arguments for
from_option.  This creates just a needless divergence between what is written
and what is printed.  Also, removing it frees the name for maybe introducing a
function or notation `default` with a type like `T -> option T -> T`.