`max`/`min`

[gebner]

trafficstars

From #348: Lean 4 defines max and min in the prelude, while Lean 3 (as of https://github.com/leanprover-community/lean/pull/609) defines them differently as part of linear_order. We will need to figure out how to resolve this conflict.

Probably the easiest thing would be to get notation typeclasses Max and Min into core.