feat(order): add lemma (#1375)

src/algebra/order.lean

@@ -164,6 +164,9 @@ lemma le_iff_le_iff_lt_iff_lt {β} [decidable_linear_order α] [decidable_linear
   {a b : α} {c d : β} : (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
 ⟨lt_iff_lt_of_le_iff_le, λ H, not_lt.symm.trans $ iff.trans (not_congr H) $ not_lt⟩
 
+lemma min_le_max [decidable_linear_order α] (a b : α) : min a b ≤ max a b :=
+le_trans (min_le_left a b) (le_max_left a b)
+
 end decidable
 
 namespace ordering