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 they simpl nicer). Done in !643 (merged)
• 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 under Permutation. Done in !643 (merged)