From 85ef7c5151beb6ab4ef7156f9772a4756033a065 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 26 Jan 2015 11:42:13 -0500
Subject: [PATCH] refactor(library/algebra/group): rename neg_add_distrib to
 neg_add, etc.

---
 library/algebra/group.lean         | 8 ++++----
 library/algebra/ordered_group.lean | 4 ++--
 library/data/int/basic.lean        | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index d9fd0cff0..e338da334 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -341,7 +341,7 @@ section add_group
       ... = a + 0 : add.right_inv
       ... = a : add_zero
 
-  theorem neg_add (a b : A) : -(a + b) = -b + -a :=
+  theorem neg_add_rev (a b : A) : -(a + b) = -b + -a :=
   neg_eq_of_add_eq_zero
     (calc
       a + b + (-b + -a) = a + (b + (-b + -a)) : add.assoc
@@ -437,7 +437,7 @@ section add_group
 
   theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b :=
   calc
-    a - (b + c) = a + (-c - b) : neg_add
+    a - (b + c) = a + (-c - b) : neg_add_rev
       ... = a - c - b : !add.assoc⁻¹
 
   theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
@@ -466,14 +466,14 @@ include s
 
   theorem neg_add_eq_sub (a b : A) : -a + b = b - a := !add.comm
 
-  theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := add.comm (-b) (-a) ▸ neg_add a b
+  theorem neg_add (a b : A) : -(a + b) = -a + -b := add.comm (-b) (-a) ▸ neg_add_rev a b
 
   theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b := !add.right_comm
 
   theorem sub_sub (a b c : A) : a - b - c = a - (b + c) :=
   calc
     a - b - c = a + (-b + -c) : add.assoc
-      ... = a + -(b + c) : {(neg_add_distrib b c)⁻¹}
+      ... = a + -(b + c) : {(neg_add b c)⁻¹}
       ... = a - (b + c) : rfl
 
   theorem add_sub_add_left_eq_sub (a b c : A) : (c + a) - (c + b) = a - b :=
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 2c9860bb2..a6b07b281 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -525,11 +525,11 @@ section
     or.elim (le.total 0 (a + b))
       (assume H2 : 0 ≤ a + b, aux2 H2)
       (assume H2 : a + b ≤ 0,
-        have H3 : -a + -b = -(a + b), from !neg_add_distrib⁻¹,
+        have H3 : -a + -b = -(a + b), from !neg_add⁻¹,
         have H4 : -(a + b) ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H2,
         calc
           |a + b| = |-(a + b)|  : abs_neg
-              ... = |-a + -b|   : neg_add_distrib
+              ... = |-a + -b|   : neg_add
               ... ≤ |-a| + |-b| : aux2 (H3⁻¹ ▸ H4)
               ... = |a| + |-b|  : abs_neg
               ... = |a| + |b|   : abs_neg)
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 82949d22e..a63a29071 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -640,7 +640,7 @@ section port_algebra
   theorem add.right_inv : ∀a : ℤ, a + -a = 0 := algebra.add.right_inv
   theorem add_neg_cancel_left : ∀a b : ℤ, a + (-a + b) = b := algebra.add_neg_cancel_left
   theorem add_neg_cancel_right : ∀a b : ℤ, a + b + -b = a := algebra.add_neg_cancel_right
-  theorem neg_add : ∀a b : ℤ, -(a + b) = -b + -a := algebra.neg_add
+  theorem neg_add_rev : ∀a b : ℤ, -(a + b) = -b + -a := algebra.neg_add_rev
   theorem eq_add_neg_of_add_eq : ∀{a b c : ℤ}, a + b = c → a = c + -b :=
     @algebra.eq_add_neg_of_add_eq _ _
   theorem eq_neg_add_of_add_eq : ∀{a b c : ℤ}, a + b = c → b = -a + c :=
@@ -681,7 +681,7 @@ section port_algebra
     @algebra.eq_iff_eq_of_sub_eq_sub _ _
   theorem sub_add_eq_sub_sub : ∀a b c : ℤ, a - (b + c) = a - b - c := algebra.sub_add_eq_sub_sub
   theorem neg_add_eq_sub : ∀a b : ℤ, -a + b = b - a := algebra.neg_add_eq_sub
-  theorem neg_add_distrib : ∀a b : ℤ, -(a + b) = -a + -b := algebra.neg_add_distrib
+  theorem neg_add : ∀a b : ℤ, -(a + b) = -a + -b := algebra.neg_add
   theorem sub_add_eq_add_sub : ∀a b c : ℤ, a - b + c = a + c - b := algebra.sub_add_eq_add_sub
   theorem sub_sub_ : ∀a b c : ℤ, a - b - c = a - (b + c) := algebra.sub_sub
   theorem add_sub_add_left_eq_sub : ∀a b c : ℤ, (c + a) - (c + b) = a - b :=