feat(library/algebra/ordered_field,library/data/int/div): prove sign a = a / abs a

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

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 :=