`sum_list_with` and `max_list_with` improvements
As discussed in !266 (comment 68380)
- Provide lemmas that show the definitions are the same as a version with
foldr
(we want to keep the current definitions because theysimpl
nicer). - Make the definitions type class opaque so that Coq does not accidentally finds type class instances because the definition is convertible to a
foldr
. - Provide instances for
Proper
underPermutation
.