From f9f4cd2197190369ff0541dca9f238efbf1e347b Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Fri, 14 Aug 2015 08:49:17 -0400
Subject: [PATCH] feat(library/algebra/ordered_field,library/data/int/div):
 prove sign a = a / abs a

---
 library/algebra/ordered_field.lean | 7 +++++++
 library/data/int/div.lean          | 8 ++++++++
 2 files changed, 15 insertions(+)

diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index 8c0d866eb..70ec48145 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -539,5 +539,12 @@ section discrete_linear_ordered_field
     apply two_pos
   end
 
+  theorem sign_eq_div_abs (a : A) : sign a = a / (abs a) :=
+  decidable.by_cases
+    (suppose a = 0, by subst a; rewrite [zero_div, sign_zero])
+    (suppose a ≠ 0,
+      have abs a ≠ 0, from assume H, this (eq_zero_of_abs_eq_zero H),
+      eq_div_of_mul_eq this !eq_sign_mul_abs⁻¹)
+
 end discrete_linear_ordered_field
 end algebra
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index e63f469b1..b5a8bacee 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -573,6 +573,14 @@ decidable.by_cases
       (take c, assume H' : a = b * c,
         by rewrite [H', neg_mul_eq_mul_neg, *!mul_div_cancel_left H1]))
 
+theorem sign_eq_div_abs (a : ℤ) : sign a = a div (abs a) :=
+decidable.by_cases
+  (suppose a = 0, by subst a)
+  (suppose a ≠ 0,
+    have abs a ≠ 0, from assume H, this (eq_zero_of_abs_eq_zero H),
+    have abs a ∣ a, from abs_dvd_of_dvd !dvd.refl,
+    eq.symm (iff.mpr (!div_eq_iff_eq_mul_left `abs a ≠ 0` this) !eq_sign_mul_abs))
+
 /- div and ordering -/
 
 theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a div b * b ≤ a :=