Commit 2021-10-09 07:26 a9643aa8

feat(order/min_max): min_cases and max_cases lemmata (#9632) These lemmata make the following type of argument work seamlessly:

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