From f7ab2780d4e96d2d17a83197b3e0ec18d4292e21 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rlewis1@andrew.cmu.edu>
Date: Tue, 16 Jun 2015 18:32:53 +1000
Subject: [PATCH] feat(library/algebra): move more theorems from reals to
 algebra)

---
 library/algebra/ordered_field.lean | 18 ++++++++++++++++++
 library/algebra/ordered_group.lean |  9 +++++++--
 2 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index e165e29e0..a093e1a4f 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -443,5 +443,23 @@ section discrete_linear_ordered_field
          have Heq [visible] : a = 0, from eq_of_le_of_ge (le_of_not_gt H) (le_of_not_gt H'),
          by rewrite [Heq, div_zero, *abs_zero, div_zero])
 
+  theorem ge_sub_of_abs_sub_le_left (H : abs (a - b) ≤ c) : a ≥ b - c :=
+    if Hz : 0 ≤ a - b then
+      (calc
+        a ≥ b : (iff.mp !sub_nonneg_iff_le) Hz
+      ... ≥ b - c : sub_le_of_nonneg _ _ (le.trans !abs_nonneg H))
+    else
+      (have Habs : b - a ≤ c, by rewrite [abs_of_neg (lt_of_not_ge Hz) at H, neg_sub at H]; apply H,
+       have Habs' : b ≤ c + a, from (iff.mp' !le_add_iff_sub_right_le) Habs,
+       (iff.mp !le_add_iff_sub_left_le) Habs')
+
+  theorem ge_sub_of_abs_sub_le_right (H : abs (a - b) ≤ c) : b ≥ a - c :=
+    ge_sub_of_abs_sub_le_left (!abs_sub ▸ H)
+
+  theorem abs_sub_square : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b :=
+    by rewrite [abs_mul_self, *mul_sub_left_distrib, *mul_sub_right_distrib,
+             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]
+
 end discrete_linear_ordered_field
 end algebra
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index c47b0252c..449996974 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -428,7 +428,7 @@ section
       ... = a      : by rewrite add_zero
 
   theorem add_le_add_three {a b c d e f : A} (H1 : a ≤ d) (H2 : b ≤ e) (H3 : c ≤ f) :
-        a + b + c ≤ d + e + f := 
+        a + b + c ≤ d + e + f :=
   begin
     apply le.trans,
     apply add_le_add,
@@ -437,6 +437,8 @@ section
     apply le.refl
   end
 
+  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)
 end
 
 structure decidable_linear_ordered_comm_group [class] (A : Type)
@@ -542,6 +544,9 @@ section
   theorem abs_lt_of_lt_of_neg_lt (H1 : a < b) (H2 : -a < b) : abs a < b :=
   abs.by_cases H1 H2
 
+  theorem ne_zero_of_abs_ne_zero {a : A} (H : abs a ≠ 0) : a ≠ 0 :=
+   assume Ha, H (Ha⁻¹ ▸ abs_zero)
+
   -- the triangle inequality
   section
     private lemma aux1 {a b : A} (H1 : a + b ≥ 0) (H2 : a ≥ 0) : abs (a + b) ≤ abs a + abs b :=
@@ -601,7 +606,7 @@ section
         ... ≤ abs (a - b) + abs b   : abs_add_le_abs_add_abs,
   algebra.le_of_add_le_add_right H1
 
-  theorem abs_add_three (a b c : A) : abs (a + b + c) ≤ abs a + abs b + abs c := 
+  theorem abs_add_three (a b c : A) : abs (a + b + c) ≤ abs a + abs b + abs c :=
     begin
       apply le.trans,
       apply abs_add_le_abs_add_abs,