From eb537daa1c920cae4ab4d5788998b17399faabf6 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rlewis1@andrew.cmu.edu>
Date: Tue, 26 May 2015 11:45:09 +1000
Subject: [PATCH] feat(library/algebra): add min/max to ordered algebraic
 structures

---
 library/algebra/order.lean         | 41 ++++++++++++++++++++++++++++++
 library/algebra/ordered_field.lean |  9 +++++++
 2 files changed, 50 insertions(+)

diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index ca80cdff59..5085627797 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -340,6 +340,47 @@ section
   theorem lt.cases_of_gt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a > b) :
     lt.cases a b t_lt t_eq t_gt = t_gt :=
   if_neg (ne.symm (ne_of_lt H)) ⬝ if_neg (lt.asymm H)
+
+  definition max (a b : A) : A :=
+  if a < b then b else a
+
+  definition min (a b : A) : A :=
+  if a < b then a else b
+
+  theorem max_a_a (a : A) : a = max a a :=
+  eq.rec_on !if_t_t rfl
+
+  theorem max.eq_right {a b : A} (H : a < b) : max a b = b :=
+  if_pos H
+
+  theorem max.eq_left {a b : A} (H : ¬ a < b) : max a b = a :=
+  if_neg H
+
+  theorem max.right_eq {a b : A} (H : a < b) : b = max a b :=
+  eq.rec_on (max.eq_right H) rfl
+
+  theorem max.left_eq {a b : A} (H : ¬ a < b) : a = max a b :=
+  eq.rec_on (max.eq_left H) rfl
+
+  theorem max.left (a b : A) : a ≤ max a b :=
+  decidable.by_cases
+    (λ h : a < b,   le_of_lt (eq.rec_on (max.right_eq h) h))
+    (λ h : ¬ a < b, eq.rec_on (max.eq_left h) !le.refl)
+
+  theorem eq_or_lt_of_not_lt (H : ¬ a < b) : a = b ∨ b < a :=
+  have H' : b = a ∨ b < a, from or.swap (lt_or_eq_of_le (le_of_not_gt H)),
+  or.elim H'
+    (take H'' : b = a, or.inl (symm H''))
+    (take H'' : b < a, or.inr H'')
+    
+  theorem max.right (a b : A) : b ≤ max a b :=
+  decidable.by_cases
+    (λ h : a < b,   eq.rec_on (max.eq_right h) !le.refl)
+    (λ h : ¬ a < b, or.rec_on (eq_or_lt_of_not_lt h)
+      (λ heq, eq.rec_on heq (eq.rec_on (max_a_a a) !le.refl))
+      (λ h : b < a,
+        have aux : a = max a b, from max.left_eq (lt.asymm h),
+        eq.rec_on aux (le_of_lt h)))
 end
 
 end algebra
diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index 3b09e4cd43..236ccbf9c4 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -253,6 +253,15 @@ section linear_ordered_field
   theorem div_lt_div_of_lt_of_neg (H : b < a) (Hc : c < 0) : a / c < b / c :=
     div_eq_mul_one_div⁻¹ ▸ div_eq_mul_one_div⁻¹ ▸ mul_lt_mul_of_neg_right H (div_neg_of_neg Hc)
 
+  theorem two_ne_zero : (1 : A) + 1 ≠ 0 :=
+    ne.symm (ne_of_lt (add_pos zero_lt_one zero_lt_one))
+
+  theorem add_halves : a / (1 + 1) + a / (1 + 1) = a :=
+    calc
+      a / (1 + 1) + a / (1 + 1) = (a + a) / (1 + 1) : div_add_div_same
+      ... = (a * 1 + a * 1) / (1 + 1) : by rewrite mul_one
+      ... = (a * (1 + 1)) / (1 + 1) : left_distrib
+      ... = a : mul_div_cancel two_ne_zero
 
 end linear_ordered_field