From 3c18f05cab4b8b5a6e5f95ff9ace21cddd64f979 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sat, 20 Feb 2016 08:27:59 -0500
Subject: [PATCH] feat(library/algebra): add some useful facts

---
 library/algebra/ordered_field.lean | 18 +++++++++---------
 library/algebra/ordered_ring.lean  |  5 ++++-
 library/algebra/ring.lean          |  7 ++++++-
 library/algebra/ring_power.lean    | 30 ++++++++++++++++++++++++++++++
 4 files changed, 49 insertions(+), 11 deletions(-)

diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index f289102de1..d89bf112fc 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -521,16 +521,16 @@ section discrete_linear_ordered_field
       apply one_div_pos_of_pos He
     end
 
+  theorem abs_div (a b : A) : abs (a / b) = abs a / abs b :=
+  decidable.by_cases
+    (suppose b = 0, by rewrite [this, abs_zero, *div_zero, abs_zero])
+    (suppose b ≠ 0,
+      have abs b ≠ 0, from assume H, this (eq_zero_of_abs_eq_zero H),
+      eq_div_of_mul_eq _ _ this
+        (show abs (a / b) * abs b = abs a, by rewrite [-abs_mul, div_mul_cancel _ `b ≠ 0`]))
+
   theorem abs_one_div (a : A) : abs (1 / a) = 1 / abs a :=
-    if H : a > 0 then
-      by rewrite [abs_of_pos H, abs_of_pos (one_div_pos_of_pos H)]
-    else
-      (if H' : a < 0 then
-          by rewrite [abs_of_neg H', abs_of_neg (one_div_neg_of_neg H'),
-                         -(division_ring.one_div_neg_eq_neg_one_div (ne_of_lt H'))]
-       else
-         assert Heq : 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])
+  by rewrite [abs_div, abs_of_nonneg (zero_le_one : 1 ≥ (0 : A))]
 
   theorem sign_eq_div_abs (a : A) : sign a = a / (abs a) :=
   decidable.by_cases
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index ff4f13eae3..5161b9cd3b 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -77,7 +77,7 @@ section
     a * b < c * b : mul_lt_mul_of_pos_right Hac pos_b
       ... ≤ c * d : mul_le_mul_of_nonneg_left Hbd nn_c
 
-theorem mul_lt_mul' (a b c d : A) (H1 : a < c) (H2 : b < d) (H3 : b ≥ 0) (H4 : c > 0) :
+  theorem mul_lt_mul' {a b c d : A} (H1 : a < c) (H2 : b < d) (H3 : b ≥ 0) (H4 : c > 0) :
         a * b < c * d :=
   calc
     a * b ≤ c * b : mul_le_mul_of_nonneg_right (le_of_lt H1) H3
@@ -103,6 +103,9 @@ theorem mul_lt_mul' (a b c d : A) (H1 : a < c) (H2 : b < d) (H3 : b ≥ 0) (H4 :
     rewrite zero_mul at  H,
     exact H
   end
+
+  theorem mul_self_lt_mul_self {a b : A} (H1 : 0 ≤ a) (H2 : a < b) : a * a < b * b :=
+  mul_lt_mul' H2 H2 H1 (lt_of_le_of_lt H1 H2)
 end
 
 structure linear_ordered_semiring [class] (A : Type)
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index 4ac09430cd..685225875d 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -327,7 +327,12 @@ structure no_zero_divisors [class] (A : Type) extends has_mul A, has_zero A :=
 
 theorem eq_zero_or_eq_zero_of_mul_eq_zero {A : Type} [no_zero_divisors A] {a b : A}
     (H : a * b = 0) :
-  a = 0 ∨ b = 0 := !no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero H
+  a = 0 ∨ b = 0 :=
+!no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero H
+
+theorem eq_zero_of_mul_self_eq_zero {A : Type} [no_zero_divisors A] {a : A} (H : a * a = 0) :
+  a = 0 :=
+or.elim (eq_zero_or_eq_zero_of_mul_eq_zero H) (assume H', H') (assume H', H')
 
 structure integral_domain [class] (A : Type) extends comm_ring A, no_zero_divisors A,
     zero_ne_one_class A
diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean
index dbf2bf56e2..c50d7b895d 100644
--- a/library/algebra/ring_power.lean
+++ b/library/algebra/ring_power.lean
@@ -124,6 +124,27 @@ begin
   apply le_of_lt xpos
 end
 
+theorem squared_lt_squared {x y : A} (H1 : 0 ≤ x) (H2 : x < y) : x^2 < y^2 :=
+by rewrite [*pow_two]; apply mul_self_lt_mul_self H1 H2
+
+theorem squared_le_squared {x y : A} (H1 : 0 ≤ x) (H2 : x ≤ y) : x^2 ≤ y^2 :=
+or.elim (lt_or_eq_of_le H2)
+  (assume xlty, le_of_lt (squared_lt_squared H1 xlty))
+  (assume xeqy, by rewrite xeqy; apply le.refl)
+
+theorem lt_of_squared_lt_squared {x y : A} (H1 : y ≥ 0) (H2 : x^2 < y^2) : x < y :=
+lt_of_not_ge (assume H : x ≥ y, not_le_of_gt H2 (squared_le_squared H1 H))
+
+theorem le_of_squared_le_squared {x y : A} (H1 : y ≥ 0) (H2 : x^2 ≤ y^2) : x ≤ y :=
+le_of_not_gt (assume H : x > y, not_lt_of_ge H2 (squared_lt_squared H1 H))
+
+theorem eq_of_squared_eq_squared_of_nonneg {x y : A} (H1 : x ≥ 0) (H2 : y ≥ 0) (H3 : x^2 = y^2) :
+  x = y :=
+lt.by_cases
+  (suppose x < y, absurd (eq.subst H3 (squared_lt_squared H1 this)) !lt.irrefl)
+  (suppose x = y, this)
+  (suppose x > y, absurd (eq.subst H3 (squared_lt_squared H2 this)) !lt.irrefl)
+
 end linear_ordered_semiring
 
 section decidable_linear_ordered_comm_ring
@@ -140,6 +161,15 @@ begin
   rewrite [*pow_succ, abs_mul, ih]
 end
 
+theorem squared_nonneg (x : A) : x^2 ≥ 0 := by rewrite [pow_two]; apply mul_self_nonneg
+
+theorem eq_zero_of_squared_eq_zero {x : A} (H : x^2 = 0) : x = 0 :=
+by rewrite [pow_two at H]; exact eq_zero_of_mul_self_eq_zero H
+
+theorem abs_eq_abs_of_squared_eq_squared {x y : A} (H : x^2 = y^2) : abs x = abs y :=
+have (abs x)^2 = (abs y)^2, by rewrite [-+abs_pow, H],
+eq_of_squared_eq_squared_of_nonneg (abs_nonneg x) (abs_nonneg y) this
+
 end decidable_linear_ordered_comm_ring
 
 section field