From e416291135f3f82c8ffdd10f512eaed2c0dc7043 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Fri, 14 Aug 2015 13:16:07 -0400
Subject: [PATCH] feat(library/algebra/*,library/data/*): small additions and
 changes

---
 library/algebra/ordered_field.lean |  4 ++--
 library/algebra/ordered_ring.lean  |  5 ++++-
 library/data/nat/parity.lean       | 12 ++++++++++++
 library/data/rat/basic.lean        |  2 +-
 4 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index 70ec481453..24b7ad6547 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -521,7 +521,7 @@ section discrete_linear_ordered_field
     ge_sub_of_abs_sub_le_left (!abs_sub ▸ H)
 
   theorem abs_sub_square : abs (a - b) * abs (a - b) = a * a + b * b - 2 * a * b :=
-    by rewrite [abs_mul_self, *mul_sub_left_distrib, *mul_sub_right_distrib,
+    by rewrite [abs_mul_abs_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]
 
@@ -529,7 +529,7 @@ section discrete_linear_ordered_field
   begin
     apply nonneg_le_nonneg_of_squares_le,
     repeat apply abs_nonneg,
-    rewrite [*abs_sub_square, *abs_abs, *abs_mul_self],
+    rewrite [*abs_sub_square, *abs_abs, *abs_mul_abs_self],
     apply sub_le_sub_left,
     rewrite *mul.assoc,
     apply mul_le_mul_of_nonneg_left,
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index cc4eb2e8a3..ac364bd0df 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -642,8 +642,11 @@ section
                     ... = abs a * -b    : by rewrite (abs_of_nonpos H1)
                     ... = abs a * abs b : by rewrite (abs_of_nonpos H2)))
 
-  theorem abs_mul_self (a : A) : abs a * abs a = a * a :=
+  theorem abs_mul_abs_self (a : A) : abs a * abs a = a * a :=
   abs.by_cases rfl !neg_mul_neg
+
+  theorem abs_mul_self (a : A) : abs (a * a) = a * a :=
+  by rewrite [abs_mul, abs_mul_abs_self]
 end
 
 /- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
diff --git a/library/data/nat/parity.lean b/library/data/nat/parity.lean
index 10aea6c81e..2d5e2e7ea5 100644
--- a/library/data/nat/parity.lean
+++ b/library/data/nat/parity.lean
@@ -217,6 +217,18 @@ by_contradiction (suppose ¬ odd (n*m),
   assert even (n*m), from even_of_not_odd this,
   absurd `even (n * m + n)` (not_even_of_odd (odd_add_of_even_of_odd this `odd n`)))
 
+lemma even_of_even_mul_self {n} : even (n * n) → even n :=
+suppose even (n * n),
+by_contradiction (suppose odd n,
+  have odd (n * n), from odd_mul_of_odd_of_odd this this,
+  show false, from this `even (n * n)`)
+
+lemma odd_of_odd_mul_self {n} : odd (n * n) → odd n :=
+suppose odd (n * n),
+  suppose even n,
+  have even (n * n), from !even_mul_of_even_left this,
+  show false, from `odd (n * n)` this
+
 lemma eq_of_div2_of_even {n m : nat} : n div 2 = m div 2 → (even n ↔ even m) → n = m :=
 assume h₁ h₂,
  or.elim (em (even n))
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index e839c250a8..60079e6f8b 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -543,7 +543,7 @@ theorem eq_num_div_denom (a : ℚ) : a = num a / denom a :=
 have H : of_int (denom a) ≠ 0, from assume H', ne_of_gt (denom_pos a) (of_int.inj H'),
 iff.mpr (eq_div_iff_mul_eq H) (mul_denom a)
 
-theorem of_nat_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b :=
+theorem of_int_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b :=
 decidable.by_cases
   (assume bz : b = 0,
     by rewrite [bz, div_zero, int.div_zero])