feat(order/min_max): min_cases and max_cases lemmata (#9632)
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





leanprover-community/mathlib,leanprover-community/mathlib