From 82a9bc757a48eed670b54e02f02a7211ef823c9f Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Mon, 3 Aug 2015 15:01:32 -0400
Subject: [PATCH] feat(library/algebra): move theorems from real to algebra

---
 library/algebra/group.lean         | 11 ++++++++++-
 library/algebra/ordered_field.lean | 31 +++++++++++++++++++++++++++++-
 library/algebra/ordered_group.lean |  3 +++
 3 files changed, 43 insertions(+), 2 deletions(-)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index a69341bbee..5d2a6c6323 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -456,6 +456,9 @@ section add_group
   ⦃ add_right_cancel_semigroup, s,
     add_right_cancel := @add_right_cancel A s ⦄
 
+  theorem add_neg_eq_neg_add_rev {a b : A} : a + -b = -(b + -a) :=
+  by rewrite [neg_add_rev, neg_neg]
+
   /- sub -/
 
   -- TODO: derive corresponding facts for div in a field
@@ -561,7 +564,13 @@ section add_comm_group
 
   theorem sub_sub_self (a b : A) : a - (a - b) = b :=
   by rewrite [sub_eq_add_neg, neg_sub, add.comm, sub_add_cancel]
- 
+
+  theorem add_sub_comm (a b c d : A) : a + b - (c + d) = (a - c) + (b - d) :=
+    by rewrite [sub_add_eq_sub_sub, -sub_add_eq_add_sub a c b, add_sub]
+
+  theorem sub_eq_sub_add_sub (a b c : A) : a - b = c - b + (a - c) :=
+    by rewrite [add_sub, sub_add_cancel] ⬝ !add.comm
+
 end add_comm_group
 
 definition group_of_add_group (A : Type) [G : add_group A] : group A :=
diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index 13eb69bccb..756f5afef9 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -285,8 +285,11 @@ section linear_ordered_field
     exact mul_le_mul_of_nonpos_right H (le_of_lt (div_neg_of_neg Hc))
   end
 
+  theorem two_pos : (1 : A) + 1 > 0 :=
+    add_pos zero_lt_one zero_lt_one
+
   theorem two_ne_zero : (1 : A) + 1 ≠ 0 :=
-    ne.symm (ne_of_lt (add_pos zero_lt_one zero_lt_one))
+    ne.symm (ne_of_lt two_pos)
 
   notation 2 := 1 + 1
 
@@ -343,6 +346,18 @@ theorem nonneg_le_nonneg_of_squares_le  (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a
       apply div_pos_of_pos He
     end
 
+  theorem find_midpoint (H : a > b) : ∃ c : A, a > b + c ∧ c > 0 :=
+    exists.intro ((a - b) / (1 + 1))
+      (and.intro (assert H2 : a + a > (b + b) + (a - b), from calc
+        a + a > b + a : add_lt_add_right H
+        ... = b + a + b - b : add_sub_cancel
+        ... = b + b + a - b : add.right_comm
+        ... = (b + b) + (a - b) : add_sub,
+      assert H3 : (a + a) / (1 + 1) > ((b + b) + (a - b)) / (1 + 1),
+        from div_lt_div_of_lt_of_pos H2 two_pos,
+      by rewrite [div_two at H3, -div_add_div_same at H3, div_two at H3]; exact H3)
+      (pos_div_of_pos_of_pos (iff.mpr !sub_pos_iff_lt H) two_pos))
+
 end linear_ordered_field
 
 structure discrete_linear_ordered_field [class] (A : Type) extends linear_ordered_field A,
@@ -513,5 +528,19 @@ section discrete_linear_ordered_field
              sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul,
              *add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc]
 
+  theorem abs_abs_sub_abs_le_abs_sub (a b : A) : abs (abs a - abs b) ≤ abs (a - b) :=
+  begin
+    apply nonneg_le_nonneg_of_squares_le,
+    repeat apply abs_nonneg,
+    rewrite [*abs_sub_square, *abs_abs, *abs_mul_self],
+    apply sub_le_sub_left,
+    rewrite *mul.assoc,
+    apply mul_le_mul_of_nonneg_left,
+    rewrite -abs_mul,
+    apply le_abs_self,
+    apply le_of_lt,
+    apply two_pos
+  end
+
 end discrete_linear_ordered_field
 end algebra
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index f2ba5b5e83..1eeaf9ff58 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -418,6 +418,9 @@ section
 
   theorem sub_le_of_nonneg (H : b ≥ 0) : a - b ≤ a :=
    add_le_of_le_of_nonpos (le.refl a) (neg_nonpos_of_nonneg H)
+
+  theorem neg_add_neg_le_neg_of_pos {a : A} (H : a > 0) : -a + -a ≤ -a :=
+    !neg_add ▸ neg_le_neg (le_add_of_nonneg_left (le_of_lt H))
 end
 
 /- partially ordered groups with min and max -/