feat(order/min_max): min_cases and max_cases lemmata (#9632)
These lemmata make the following type of argument work seamlessly:
```lean
example (h1 : 0 ≤ x) (h2 : x ≤ 1) : min 1 x ≤ max x 0 := by cases min_cases 1 x; cases max_cases x 0; linarith
```
See similar PR #8124
