From 486bc321fff7655f864940357cd81287e4dc1435 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Tue, 23 Dec 2014 17:34:16 -0500
Subject: [PATCH] refactor(library/data/nat): rename theorems

---
 doc/lean/calc.org                 |   2 +-
 doc/lean/tutorial.org             |   4 +-
 library/algebra/ordered_ring.lean |  26 ++--
 library/algebra/ring.lean         |  28 ++--
 library/data/int/basic.lean       |  26 ++--
 library/data/int/order.lean       |   4 +-
 library/data/list/basic.lean      |  46 +++----
 library/data/nat/basic.lean       | 213 +++++++++++++++---------------
 library/data/nat/div.lean         |  38 +++---
 library/data/nat/order.lean       |  62 ++++-----
 library/data/nat/sub.lean         |  48 +++----
 tests/lean/run/class4.lean        |   4 +-
 tests/lean/run/imp_curly.lean     |   4 +-
 tests/lean/run/nat_bug5.lean      |   2 +-
 tests/lean/slow/list_elab2.lean   |   2 +-
 tests/lean/slow/nat_bug2.lean     | 152 ++++++++++-----------
 tests/lean/slow/nat_wo_hints.lean | 152 ++++++++++-----------
 17 files changed, 405 insertions(+), 408 deletions(-)

diff --git a/doc/lean/calc.org b/doc/lean/calc.org
index c74bf35f8..2a6aed1f9 100644
--- a/doc/lean/calc.org
+++ b/doc/lean/calc.org
@@ -58,7 +58,7 @@ some form of transitivity. It can even combine different relations.
   theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0
   := calc  a = b      : H1
          ... = c + 1  : H2
-         ... = succ c : add.one c
+         ... = succ c : add_one c
          ... ≠ 0      : succ_ne_zero c
 #+END_SRC
 
diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org
index 932c4de85..764595edd 100644
--- a/doc/lean/tutorial.org
+++ b/doc/lean/tutorial.org
@@ -760,7 +760,7 @@ of two even numbers is an even number.
     exists.intro (w1 + w2)
       (calc a + b  =  2*w1 + b      : {Hw1}
               ...  =  2*w1 + 2*w2   : {Hw2}
-              ...  =  2*(w1 + w2)   : eq.symm !mul.distr_left)))
+              ...  =  2*(w1 + w2)   : eq.symm !mul.left_distrib)))
 
 #+END_SRC
 
@@ -780,5 +780,5 @@ With this macro we can write the example above in a more natural way
     exists.intro (w1 + w2)
       (calc a + b  =  2*w1 + b      : {Hw1}
               ...  =  2*w1 + 2*w2   : {Hw2}
-              ...  =  2*(w1 + w2)   : eq.symm !mul.distr_left)
+              ...  =  2*(w1 + w2)   : eq.symm !mul.left_distrib)
 #+END_SRC
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index 7d9b4069b..38ee26ad0 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -57,15 +57,15 @@ section
 
   theorem mul_nonneg_of_nonneg_of_nonneg {a b : A} (Ha : a ≥ 0) (Hb : b ≥ 0) : a * b ≥ 0 :=
   have H : 0 * b ≤ a * b, from mul_le_mul_of_nonneg_right Ha Hb,
-  !zero_mul_eq ▸ H
+  !zero_mul ▸ H
 
   theorem mul_nonpos_of_nonneg_of_nonpos {a b : A} (Ha : a ≥ 0) (Hb : b ≤ 0) : a * b ≤ 0 :=
   have H : a * b ≤ a * 0, from mul_le_mul_of_nonneg_left Hb Ha,
-  !mul_zero_eq ▸ H
+  !mul_zero ▸ H
 
   theorem mul_nonpos_of_nonpos_of_nonneg {a b : A} (Ha : a ≤ 0) (Hb : b ≥ 0) : a * b ≤ 0 :=
   have H : a * b ≤ 0 * b, from mul_le_mul_of_nonneg_right Ha Hb,
-  !zero_mul_eq ▸ H
+  !zero_mul ▸ H
 
   theorem mul_lt_mul_of_pos_left {a b c : A} (Hab : a < b) (Hc : 0 < c) :
     c * a < c * b := !ordered_semiring.mul_lt_mul_left Hab Hc
@@ -82,15 +82,15 @@ section
 
   theorem mul_pos_of_pos_of_pos {a b : A} (Ha : a > 0) (Hb : b > 0) : a * b > 0 :=
   have H : 0 * b < a * b, from mul_lt_mul_of_pos_right Ha Hb,
-  !zero_mul_eq ▸ H
+  !zero_mul ▸ H
 
   theorem mul_neg_of_pos_of_neg {a b : A} (Ha : a > 0) (Hb : b < 0) : a * b < 0 :=
   have H : a * b < a * 0, from mul_lt_mul_of_pos_left Hb Ha,
-  !mul_zero_eq ▸ H
+  !mul_zero ▸ H
 
   theorem mul_neg_of_neg_of_pos {a b : A} (Ha : a < 0) (Hb : b > 0) : a * b < 0 :=
   have H : a * b < 0 * b, from mul_lt_mul_of_pos_right Ha Hb,
-  !zero_mul_eq ▸ H
+  !zero_mul ▸ H
 
 end
 
@@ -158,7 +158,7 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
   ordered_ring.add_left_id ordered_ring.add_right_id ordered_ring.add_comm ordered_ring.mul
   ordered_ring.mul_assoc !ordered_ring.one ordered_ring.mul_left_id ordered_ring.mul_right_id
   ordered_ring.left_distrib ordered_ring.right_distrib
-  zero_mul_eq mul_zero_eq !ordered_ring.zero_ne_one
+  zero_mul mul_zero !ordered_ring.zero_ne_one
   (@add.left_cancel A _) (@add.right_cancel A _)
   ordered_ring.le ordered_ring.le_refl ordered_ring.le_trans ordered_ring.le_antisym
   ordered_ring.lt ordered_ring.lt_iff_le_ne ordered_ring.add_le_add_left
@@ -227,7 +227,7 @@ section
   iff.mp !neg_le_neg_iff_le H2
 
   theorem mul_nonneg_of_nonpos_of_nonpos {a b : A} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a * b :=
-  !zero_mul_eq ▸ mul_le_mul_of_nonpos_right Ha Hb
+  !zero_mul ▸ mul_le_mul_of_nonpos_right Ha Hb
 
   theorem mul_lt_mul_of_neg_left {a b c : A} (H : b < a) (Hc : c < 0) : c * a < c * b :=
   have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc,
@@ -242,7 +242,7 @@ section
   iff.mp !neg_lt_neg_iff_lt H2
 
   theorem mul_pos_of_neg_of_neg {a b : A} (Ha : a < 0) (Hb : b < 0) : 0 < a * b :=
-  !zero_mul_eq ▸ mul_lt_mul_of_neg_right Ha Hb
+  !zero_mul ▸ mul_lt_mul_of_neg_right Ha Hb
 
 end
 
@@ -291,7 +291,7 @@ section
   Adding the explicit arguments to lt_or_eq_or_lt_cases does not seem to help at all. (The proof
     still works if all the instances are replaced by "lt_or_eq_or_lt_cases" alone.)
 
-  Adding an extra "proof ... qed" around "!mul_zero_eq ▸ Hb⁻¹ ▸ Hab" fails with "value has
+  Adding an extra "proof ... qed" around "!mul_zero ▸ Hb⁻¹ ▸ Hab" fails with "value has
   metavariables". I am not sure why.
   -/
   theorem pos_and_pos_or_neg_and_neg_of_mul_pos (Hab : a * b > 0) :
@@ -301,17 +301,17 @@ section
       lt_or_eq_or_lt_cases
         (assume Hb : 0 < b, or.inl (and.intro Ha Hb))
         (assume Hb : 0 = b,
-          absurd (!mul_zero_eq ▸ Hb⁻¹ ▸ Hab) (lt.irrefl 0))
+          absurd (!mul_zero ▸ Hb⁻¹ ▸ Hab) (lt.irrefl 0))
         (assume Hb : b < 0,
           absurd Hab (not_lt_of_lt (mul_neg_of_pos_of_neg Ha Hb))))
     (assume Ha : 0 = a,
-      absurd (!zero_mul_eq ▸ Ha⁻¹ ▸ Hab) (lt.irrefl 0))
+      absurd (!zero_mul ▸ Ha⁻¹ ▸ Hab) (lt.irrefl 0))
     (assume Ha : a < 0,
       lt_or_eq_or_lt_cases
         (assume Hb : 0 < b,
           absurd Hab (not_lt_of_lt (mul_neg_of_neg_of_pos Ha Hb)))
         (assume Hb : 0 = b,
-          absurd (!mul_zero_eq ▸ Hb⁻¹ ▸ Hab) (lt.irrefl 0))
+          absurd (!mul_zero ▸ Hb⁻¹ ▸ Hab) (lt.irrefl 0))
         (assume Hb : b < 0, or.inr (and.intro Ha Hb)))
 
   set_option pp.coercions true
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index cec35532a..47c4d87f8 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -30,12 +30,12 @@ theorem left_distrib [s : distrib A] (a b c : A) : a * (b + c) = a * b + a * c :
 theorem right_distrib [s: distrib A] (a b c : A) : (a + b) * c = a * c + b * c :=
 !distrib.right_distrib
 
-structure mul_zero [class] (A : Type) extends has_mul A, has_zero A :=
-(zero_mul_eq : ∀a, mul zero a = zero)
-(mul_zero_eq : ∀a, mul a zero = zero)
+structure mul_zero_class [class] (A : Type) extends has_mul A, has_zero A :=
+(zero_mul : ∀a, mul zero a = zero)
+(mul_zero : ∀a, mul a zero = zero)
 
-theorem zero_mul_eq [s : mul_zero A] (a : A) : 0 * a = 0 := !mul_zero.zero_mul_eq
-theorem mul_zero_eq [s : mul_zero A] (a : A) : a * 0 = 0 := !mul_zero.mul_zero_eq
+theorem zero_mul [s : mul_zero_class A] (a : A) : 0 * a = 0 := !mul_zero_class.zero_mul
+theorem mul_zero [s : mul_zero_class A] (a : A) : a * 0 = 0 := !mul_zero_class.mul_zero
 
 structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A :=
 (zero_ne_one : zero ≠ one)
@@ -44,8 +44,8 @@ theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := @zero_ne_one_class.zer
 
 /- semiring -/
 
-structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A, mul_zero A,
-    zero_ne_one_class A
+structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A,
+    mul_zero_class A, zero_ne_one_class A
 
 section semiring
 
@@ -54,12 +54,12 @@ section semiring
 
   theorem ne_zero_of_mul_ne_zero_right {a b : A} (H : a * b ≠ 0) : a ≠ 0 :=
   assume H1 : a = 0,
-  have H2 : a * b = 0, from H1⁻¹ ▸ zero_mul_eq b,
+  have H2 : a * b = 0, from H1⁻¹ ▸ zero_mul b,
   H H2
 
   theorem ne_zero_of_mul_ne_zero_left {a b : A} (H : a * b ≠ 0) : b ≠ 0 :=
   assume H1 : b = 0,
-  have H2 : a * b = 0, from H1⁻¹ ▸ mul_zero_eq a,
+  have H2 : a * b = 0, from H1⁻¹ ▸ mul_zero a,
   H H2
 
 end semiring
@@ -100,9 +100,9 @@ section comm_semiring
                 ... = c : H₄)))
 
   theorem eq_zero_of_zero_dvd {H : 0 | a} : a = 0 :=
-    dvd.elim H (take c, assume H' : 0 * c = a, (H')⁻¹ ⬝ !zero_mul_eq)
+    dvd.elim H (take c, assume H' : 0 * c = a, (H')⁻¹ ⬝ !zero_mul)
 
-  theorem dvd_zero : a | 0 := dvd.intro !mul_zero_eq
+  theorem dvd_zero : a | 0 := dvd.intro !mul_zero
 
   theorem one_dvd : 1 | a := dvd.intro !mul.left_id
 
@@ -186,14 +186,14 @@ section
     (calc
       a * b + -a * b = (a + -a) * b : right_distrib
         ... = 0 * b : add.right_inv
-        ... = 0 : zero_mul_eq)
+        ... = 0 : zero_mul)
 
   theorem neg_mul_eq_mul_neg : -(a * b) = a * -b :=
   neg_eq_of_add_eq_zero
     (calc
       a * b + a * -b = a * (b + -b) : left_distrib
         ... = a * 0 : add.right_inv
-        ... = 0 : mul_zero_eq)
+        ... = 0 : mul_zero)
 
   theorem neg_mul_neg_eq : -a * -b = a * b :=
   calc
@@ -234,7 +234,7 @@ definition comm_ring.to_comm_semiring [instance] [s : comm_ring A] : comm_semiri
 comm_semiring.mk comm_ring.add comm_ring.add_assoc (@comm_ring.zero A s)
   comm_ring.add_left_id comm_ring.add_right_id comm_ring.add_comm comm_ring.mul comm_ring.mul_assoc
   (@comm_ring.one A s) comm_ring.mul_left_id comm_ring.mul_right_id comm_ring.left_distrib
-  comm_ring.right_distrib zero_mul_eq mul_zero_eq (@comm_ring.zero_ne_one A s)
+  comm_ring.right_distrib zero_mul mul_zero (@comm_ring.zero_ne_one A s)
   comm_ring.mul_comm
 
 section
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index f4088b95d..cb2d77d33 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -220,12 +220,12 @@ or.elim (@le_or_gt n m)
     H1⁻¹ ▸
       (calc
         m - n + n = m : add_sub_ge_left H
-          ... = 0 + m : add.zero_left))
+          ... = 0 + m : add.left_id))
   (take H : m < n,
     have H1 : repr (sub_nat_nat m n) = (0, succ (pred (n - m))), from sub_nat_nat_of_lt H ▸ rfl,
     H1⁻¹ ▸
       (calc
-        0 + n = n : add.zero_left
+        0 + n = n : add.left_id
           ... = n - m + m : add_sub_ge_left (lt_imp_le H)
           ... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_gt H))⁻¹))
 
@@ -336,7 +336,7 @@ cases_on a
           from !repr_sub_nat_nat,
         have H2 : padd (repr (of_nat m)) (repr (neg_succ_of_nat n')) = (m, 0 + succ n'),
           from rfl,
-        (!add.zero_left ▸ H2)⁻¹ ▸ H1))
+        (!add.left_id ▸ H2)⁻¹ ▸ H1))
   (take m',
     cases_on b
       (take n,
@@ -344,7 +344,7 @@ cases_on a
           from !repr_sub_nat_nat,
         have H2 : padd (repr (neg_succ_of_nat m')) (repr (of_nat n)) = (0 + n, succ m'),
           from rfl,
-        (!add.zero_left ▸ H2)⁻¹ ▸ H1)
+        (!add.left_id ▸ H2)⁻¹ ▸ H1)
        (take n',!repr_sub_nat_nat))
 
 theorem padd_congr {p p' q q' : ℕ × ℕ} (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' :=
@@ -486,12 +486,12 @@ cases_on a
       (take n,
         (calc
           pmul (repr m) (repr n) = (m * n + 0 * 0, m * 0 + 0 * n) : rfl
-            ... = (m * n + 0 * 0, m * 0 + 0) : mul.zero_left)⁻¹)
+            ... = (m * n + 0 * 0, m * 0 + 0) : zero_mul)⁻¹)
       (take n',
         (calc
           pmul (repr m) (repr (neg_succ_of_nat n')) =
               (m * 0 + 0 * succ n', m * succ n' + 0 * 0) : rfl
-            ... = (m * 0 + 0, m * succ n' + 0 * 0) : mul.zero_left
+            ... = (m * 0 + 0, m * succ n' + 0 * 0) : zero_mul
             ... = repr (mul m (neg_succ_of_nat n')) : repr_neg_of_nat)⁻¹))
   (take m',
     cases_on b
@@ -499,15 +499,15 @@ cases_on a
         (calc
           pmul (repr (neg_succ_of_nat m')) (repr n) =
               (0 * n + succ m' * 0, 0 * 0 + succ m' * n) : rfl
-            ... = (0 + succ m' * 0, 0 * 0 + succ m' * n) : mul.zero_left
-            ... = (0 + succ m' * 0, succ m' * n) : add.zero_left
+            ... = (0 + succ m' * 0, 0 * 0 + succ m' * n) : zero_mul
+            ... = (0 + succ m' * 0, succ m' * n) : nat.add.left_id
             ... = repr (mul (neg_succ_of_nat m') n) : repr_neg_of_nat)⁻¹)
       (take n',
         (calc
           pmul (repr (neg_succ_of_nat m')) (repr (neg_succ_of_nat n')) =
               (0 + succ m' * succ n', 0 * succ n') : rfl
-            ... = (succ m' * succ n', 0 * succ n') : add.zero_left
-            ... = (succ m' * succ n', 0) : mul.zero_left
+            ... = (succ m' * succ n', 0 * succ n') : nat.add.left_id
+            ... = (succ m' * succ n', 0) : zero_mul
             ... = repr (mul (neg_succ_of_nat m') (neg_succ_of_nat n')) : rfl)⁻¹))
 
 theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
@@ -595,7 +595,7 @@ have H2 : (nat_abs a) * (nat_abs b) = nat.zero, from
     (nat_abs a) * (nat_abs b) = (nat_abs (a * b)) : (mul_nat_abs a b)⁻¹
       ... = (nat_abs 0) : {H}
       ... = nat.zero : nat_abs_of_nat nat.zero,
-have H3 : (nat_abs a) = nat.zero ∨ (nat_abs b) = nat.zero, from mul.eq_zero H2,
+have H3 : (nat_abs a) = nat.zero ∨ (nat_abs b) = nat.zero, from eq_zero_or_eq_zero_of_mul_eq_zero H2,
 or_of_or_of_imp_of_imp H3
   (assume H : (nat_abs a) = nat.zero, nat_abs_eq_zero H)
   (assume H : (nat_abs b) = nat.zero, nat_abs_eq_zero H)
@@ -708,8 +708,8 @@ context port_algebra
   theorem dvd_of_mul_left_dvd : ∀{a b c : ℤ}, a * b | c → b | c :=
     @algebra.dvd_of_mul_left_dvd _ _
   theorem dvd_add : ∀{a b c : ℤ}, a | b → a | c → a | b + c := @algebra.dvd_add _ _
-  theorem zero_mul_eq : ∀a : ℤ, 0 * a = 0 := algebra.zero_mul_eq
-  theorem mul_zero_eq : ∀a : ℤ, a * 0 = 0 := algebra.mul_zero_eq
+  theorem zero_mul : ∀a : ℤ, 0 * a = 0 := algebra.zero_mul
+  theorem mul_zero : ∀a : ℤ, a * 0 = 0 := algebra.mul_zero
   theorem neg_mul_eq_neg_mul : ∀a b : ℤ, -(a * b) = -a * b := algebra.neg_mul_eq_neg_mul
   theorem neg_mul_eq_mul_neg : ∀a b : ℤ, -(a * b) = a * -b := algebra.neg_mul_eq_mul_neg
   theorem neg_mul_neg_eq : ∀a b : ℤ, -a * -b = a * b := algebra.neg_mul_neg_eq
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 00c1934d6..88f5f569d 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -10,7 +10,7 @@ The order relation on the integers, and the sign function.
 
 import .basic
 
-open nat (hiding case)
+open nat
 open decidable
 open fake_simplifier
 open int eq.ops
@@ -81,7 +81,7 @@ have H3 : a + of_nat (n + m) = a + 0, from
       ... = a + 0 : (add.right_id a)⁻¹,
 have H4 : of_nat (n + m) = of_nat 0, from add.left_cancel H3,
 have H5 : n + m = 0, from of_nat_inj H4,
-have H6 : n = 0, from nat.add.eq_zero_left H5,
+have H6 : n = 0, from nat.eq_zero_of_add_eq_zero_right H5,
 show a = b, from
   calc
     a = a + of_nat 0 : (add.right_id a)⁻¹
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 02cc4419a..c918f9ec1 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -1,14 +1,15 @@
-----------------------------------------------------------------------------------------------------
---- Copyright (c) 2014 Parikshit Khanna. All rights reserved.
---- Released under Apache 2.0 license as described in the file LICENSE.
---- Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura
-----------------------------------------------------------------------------------------------------
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.list.basic
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura
+
+Basic properties of lists.
+-/
+
 import logic tools.helper_tactics data.nat.basic
 
--- Theory list
--- ===========
---
--- Basic properties of lists.
 open eq.ops helper_tactics nat
 
 inductive list (T : Type) : Type :=
@@ -21,8 +22,7 @@ notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 
 variable {T : Type}
 
--- Concat
--- ------
+/- append -/
 
 definition append (s t : list T) : list T :=
 rec t (λx l u, x::u) s
@@ -39,8 +39,7 @@ induction_on t rfl (λx l H, H ▸ rfl)
 theorem append.assoc (s t u : list T) : s ++ t ++ u = s ++ (t ++ u) :=
 induction_on s rfl (λx l H, H ▸ rfl)
 
--- Length
--- ------
+/- length -/
 
 definition length : list T → nat :=
 rec 0 (λx l m, succ m)
@@ -50,12 +49,11 @@ theorem length.nil : length (@nil T) = 0
 theorem length.cons (x : T) (t : list T) : length (x::t) = succ (length t)
 
 theorem length.append (s t : list T) : length (s ++ t) = length s + length t :=
-induction_on s (!add.zero_left⁻¹) (λx s H, !add.succ_left⁻¹ ▸ H ▸ rfl)
+induction_on s (!add.left_id⁻¹) (λx s H, !add.succ_left⁻¹ ▸ H ▸ rfl)
 
 -- add_rewrite length_nil length_cons
 
--- Append
--- ------
+/- concat -/
 
 definition concat (x : T) : list T → list T :=
 rec [x] (λy l l', y::l')
@@ -68,8 +66,7 @@ theorem concat.eq_append (x : T) (l : list T) : concat x l = l ++ [x]
 
 -- add_rewrite append_nil append_cons
 
--- Reverse
--- -------
+/- reverse -/
 
 definition reverse : list T → list T :=
 rec nil (λx l r, r ++ [x])
@@ -95,8 +92,7 @@ induction_on l rfl
     concat x (y::l') = (y::l') ++ [x]                   : !concat.eq_append
                  ... = reverse (reverse (y::l')) ++ [x] : {!reverse.reverse⁻¹})
 
--- Head and tail
--- -------------
+/- head and tail -/
 
 definition head (x : T) : list T → T :=
 rec x (λx l h, x)
@@ -126,8 +122,7 @@ cases_on l
   (assume H : nil ≠ nil, absurd rfl H)
   (take x l, assume H : x::l ≠ nil, rfl)
 
--- List membership
--- ---------------
+/- list membership -/
 
 definition mem (x : T) : list T → Prop :=
 rec false (λy l H, x = y ∨ H)
@@ -206,8 +201,8 @@ rec_on l
               iff.elim_right (not_iff_not_of_iff !mem.cons) H1,
             decidable.inr H2)))
 
--- Find
--- ----
+/- find -/
+
 section
 variable [H : decidable_eq T]
 include H
@@ -234,8 +229,7 @@ rec_on l
                   ... = length (y::l)                        : !length.cons⁻¹)
 end
 
--- nth element
--- -----------
+/- nth element -/
 
 definition nth (x : T) (l : list T) (n : nat) : T :=
 nat.rec (λl, head x l) (λm f l, f (tail l)) n l
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index f32bcf4d8..f7fbb85ba 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -1,8 +1,12 @@
---- Copyright (c) 2014 Floris van Doorn. All rights reserved.
---- Released under Apache 2.0 license as described in the file LICENSE.
---- Author: Floris van Doorn, Leonardo de Moura
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 
--- Basic operations on the natural numbers.
+Module: data.nat.basic
+Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
+
+Basic operations on the natural numbers.
+-/
 
 import logic.connectives data.num algebra.binary
 
@@ -10,6 +14,8 @@ open eq.ops binary
 
 namespace nat
 
+/- a variant of add, defined by recursion on the first argument -/
+
 definition addl (x y : ℕ) : ℕ :=
 nat.rec y (λ n r, succ r) x
 infix `⊕`:65 := addl
@@ -40,8 +46,7 @@ nat.induction_on x
                    ...  = succ (succ x₁ ⊕ y₁) : {ih₂}
                    ...  = succ x₁ ⊕ succ y₁   : addl.succ_right))
 
--- Successor and predecessor
--- -------------------------
+/- successor and predecessor -/
 
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
 assume H, no_confusion H
@@ -56,18 +61,15 @@ rfl
 
 irreducible pred
 
-theorem zero_or_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
+theorem eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
 induction_on n
   (or.inl rfl)
   (take m IH, or.inr
     (show succ m = succ (pred (succ m)), from congr_arg succ !pred.succ⁻¹))
 
-theorem zero_or_exists_succ (n : ℕ) : n = 0 ∨ ∃k, n = succ k :=
-or_of_or_of_imp_of_imp (zero_or_succ_pred n) (assume H, H)
-    (assume H : n = succ (pred n), exists.intro (pred n) H)
-
-theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n :=
-induction_on n H1 (take m IH, H2 m)
+--theorem eq_zero_or_exists_eq_succ (n : ℕ) : n = 0 ∨ ∃k, n = succ k :=
+--or_of_or_of_imp_of_imp (eq_zero_or_eq_succ_pred n) (assume H, H)
+--    (assume H : n = succ (pred n), exists.intro (pred n) H)
 
 theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
 no_confusion H (λe, e)
@@ -79,11 +81,9 @@ induction_on n
     absurd H ne)
   (take k IH H, IH (succ.inj H))
 
-
 theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
-or.elim (zero_or_succ_pred n)
-  (take H3 : n = 0, H1 H3)
-  (take H3 : n = succ (pred n), H2 (pred n) H3)
+have H : n = n → B, from cases_on n H1 H2,
+H rfl
 
 theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1)
     (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a :=
@@ -103,60 +103,65 @@ have general : ∀m, P n m, from induction_on n
   (take k : ℕ,
     assume IH : ∀m, P k m,
     take m : ℕ,
+    cases_on m (H2 k) (take l, (H3 k l (IH l)))),
+general m
+
+/-
     discriminate
       (assume Hm : m = 0, Hm⁻¹ ▸ (H2 k))
       (take l : ℕ, assume Hm : m = succ l, Hm⁻¹ ▸ (H3 k l (IH l)))),
 general m
+-/
 
--- Addition
--- --------
-theorem add.zero_right (n : ℕ) : n + 0 = n :=
+/- addition -/
+
+theorem add.right_id (n : ℕ) : n + 0 = n :=
 rfl
 
-theorem add.succ_right (n m : ℕ) : n + succ m = succ (n + m) :=
+theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) :=
 rfl
 
 irreducible add
 
-theorem add.zero_left (n : ℕ) : 0 + n = n :=
+theorem add.left_id (n : ℕ) : 0 + n = n :=
 induction_on n
-    !add.zero_right
+    !add.right_id
     (take m IH, show 0 + succ m = succ m, from
       calc
-        0 + succ m = succ (0 + m) : add.succ_right
+        0 + succ m = succ (0 + m) : add_succ
                ... = succ m       : IH)
 
 theorem add.succ_left (n m : ℕ) : (succ n) + m = succ (n + m) :=
 induction_on m
-    (!add.zero_right ▸ !add.zero_right)
+    (!add.right_id ▸ !add.right_id)
     (take k IH, calc
-      succ n + succ k = succ (succ n + k)    : add.succ_right
+      succ n + succ k = succ (succ n + k)    : add_succ
                   ... = succ (succ (n + k))  : IH
-                  ... = succ (n + succ k)    : add.succ_right)
+                  ... = succ (n + succ k)    : add_succ)
 
 theorem add.comm (n m : ℕ) : n + m = m + n :=
 induction_on m
-    (!add.zero_right ⬝ !add.zero_left⁻¹)
+    (!add.right_id ⬝ !add.left_id⁻¹)
     (take k IH, calc
-        n + succ k = succ (n+k)   : add.succ_right
+        n + succ k = succ (n+k)   : add_succ
                ... = succ (k + n) : IH
                ... = succ k + n   : add.succ_left)
 
-theorem add.move_succ (n m : ℕ) : succ n + m = n + succ m :=
-!add.succ_left ⬝ !add.succ_right⁻¹
+theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m :=
+!add.succ_left ⬝ !add_succ⁻¹
 
-theorem add.comm_succ (n m : ℕ) : n + succ m = m + succ n :=
-!add.move_succ⁻¹ ⬝ !add.comm
+-- theorem add.comm_succ (n m : ℕ) : n + succ m = m + succ n :=
+-- !succ_add_eq_add_succ⁻¹ ⬝ !add.comm
 
 theorem add.assoc (n m k : ℕ) : (n + m) + k = n + (m + k) :=
 induction_on k
-    (!add.zero_right ▸ !add.zero_right)
+    (!add.right_id ▸ !add.right_id)
     (take l IH,
       calc
-        (n + m) + succ l = succ ((n + m) + l)  : add.succ_right
+        (n + m) + succ l = succ ((n + m) + l)  : add_succ
                      ... = succ (n + (m + l))  : IH
-                     ... = n + succ (m + l)    : add.succ_right
-                     ... = n + (m + succ l)    : add.succ_right)
+                     ... = n + succ (m + l)    : add_succ
+                     ... = n + (m + succ l)    : add_succ)
 
 theorem add.left_comm (n m k : ℕ) : n + (m + k) = m + (n + k) :=
 left_comm add.comm add.assoc n m k
@@ -169,7 +174,7 @@ right_comm add.comm add.assoc n m k
 theorem add.cancel_left {n m k : ℕ} : n + m = n + k → m = k :=
 induction_on n
   (take H : 0 + m = 0 + k,
-    !add.zero_left⁻¹ ⬝ H ⬝ !add.zero_left)
+    !add.left_id⁻¹ ⬝ H ⬝ !add.left_id)
   (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
     have H2 : succ (n + m) = succ (n + k),
     from calc
@@ -183,7 +188,7 @@ theorem add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k :=
 have H2 : m + n = m + k, from !add.comm ⬝ H ⬝ !add.comm,
   add.cancel_left H2
 
-theorem add.eq_zero_left {n m : ℕ} : n + m = 0 → n = 0 :=
+theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 :=
 induction_on n
   (take (H : 0 + m = 0), rfl)
   (take k IH,
@@ -194,97 +199,97 @@ induction_on n
                   ... = 0          : H)
       !succ_ne_zero)
 
-theorem add.eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 :=
-add.eq_zero_left (!add.comm ⬝ H)
+theorem eq_zero_of_add_eq_zero_left {n m : ℕ} (H : n + m = 0) : m = 0 :=
+eq_zero_of_add_eq_zero_right (!add.comm ⬝ H)
 
 theorem add.eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 :=
-and.intro (add.eq_zero_left H) (add.eq_zero_right H)
+and.intro (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H)
 
 -- ### misc
 
-theorem add.one (n : ℕ) : n + 1 = succ n :=
-!add.zero_right ▸ !add.succ_right
+theorem add_one (n : ℕ) : n + 1 = succ n :=
+!add.right_id ▸ !add_succ
 
-theorem add.one_left (n : ℕ) : 1 + n = succ n :=
-!add.zero_left ▸ !add.succ_left
+theorem one_add (n : ℕ) : 1 + n = succ n :=
+!add.left_id ▸ !add.succ_left
 
 -- TODO: rename? remove?
-theorem induction_plus_one {P : nat → Prop} (a : ℕ) (H1 : P 0)
-    (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a :=
-nat.rec H1 (take n IH, !add.one ▸ (H2 n IH)) a
+-- theorem induction_plus_one {P : nat → Prop} (a : ℕ) (H1 : P 0)
+--     (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a :=
+-- nat.rec H1 (take n IH, !add.one ▸ (H2 n IH)) a
 
--- Multiplication
--- --------------
+/- multiplication -/
 
-theorem mul.zero_right (n : ℕ) : n * 0 = 0 :=
+theorem mul_zero (n : ℕ) : n * 0 = 0 :=
 rfl
 
-theorem mul.succ_right (n m : ℕ) : n * succ m = n * m + n :=
+theorem mul_succ (n m : ℕ) : n * succ m = n * m + n :=
 rfl
 
 irreducible mul
 
 -- ### commutativity, distributivity, associativity, identity
 
-theorem mul.zero_left (n : ℕ) : 0 * n = 0 :=
+theorem zero_mul (n : ℕ) : 0 * n = 0 :=
 induction_on n
-  !mul.zero_right
-  (take m IH, !mul.succ_right ⬝ !add.zero_right ⬝ IH)
+  !mul_zero
+  (take m IH, !mul_succ ⬝ !add.right_id ⬝ IH)
 
-theorem mul.succ_left (n m : ℕ) : (succ n) * m = (n * m) + m :=
+theorem succ_mul (n m : ℕ) : (succ n) * m = (n * m) + m :=
 induction_on m
-  (!mul.zero_right ⬝ !mul.zero_right⁻¹ ⬝ !add.zero_right⁻¹)
+  (!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add.right_id⁻¹)
   (take k IH, calc
-    succ n * succ k = (succ n * k) + succ n   : mul.succ_right
-                ... = (n * k) + k + succ n    : IH
-                ... = (n * k) + (k + succ n)  : add.assoc
-                ... = (n * k) + (n + succ k)  : add.comm_succ
-                ... = (n * k) + n + succ k    : add.assoc
-                ... = (n * succ k) + succ k   : mul.succ_right)
+    succ n * succ k = succ n * k + succ n   : mul_succ
+                ... = n * k + k + succ n    : IH
+                ... = n * k + (k + succ n)  : add.assoc
+                ... = n * k + (succ n + k)  : add.comm
+                ... = n * k + (n + succ k)  : succ_add_eq_add_succ
+                ... = n * k + n + succ k    : add.assoc
+                ... = n * succ k + succ k   : mul_succ)
 
 theorem mul.comm (n m : ℕ) : n * m = m * n :=
 induction_on m
-  (!mul.zero_right ⬝ !mul.zero_left⁻¹)
+  (!mul_zero ⬝ !zero_mul⁻¹)
   (take k IH, calc
-    n * succ k = n * k + n    : mul.succ_right
+    n * succ k = n * k + n    : mul_succ
            ... = k * n + n    : IH
-           ... = (succ k) * n : mul.succ_left)
+           ... = (succ k) * n : succ_mul)
 
-theorem mul.distr_right (n m k : ℕ) : (n + m) * k = n * k + m * k :=
+theorem mul.right_distrib (n m k : ℕ) : (n + m) * k = n * k + m * k :=
 induction_on k
   (calc
-    (n + m) * 0 = 0             : mul.zero_right
-            ... = 0 + 0         : add.zero_right
-            ... = n * 0 + 0     : mul.zero_right
-            ... = n * 0 + m * 0 : mul.zero_right)
+    (n + m) * 0 = 0             : mul_zero
+            ... = 0 + 0         : add.right_id
+            ... = n * 0 + 0     : mul_zero
+            ... = n * 0 + m * 0 : mul_zero)
   (take l IH, calc
-    (n + m) * succ l = (n + m) * l + (n + m)    : mul.succ_right
+    (n + m) * succ l = (n + m) * l + (n + m)    : mul_succ
                  ... = n * l + m * l + (n + m)  : IH
                  ... = n * l + m * l + n + m    : add.assoc
                  ... = n * l + n + m * l + m    : add.right_comm
                  ... = n * l + n + (m * l + m)  : add.assoc
-                 ... = n * succ l + (m * l + m) : mul.succ_right
-                 ... = n * succ l + m * succ l  : mul.succ_right)
+                 ... = n * succ l + (m * l + m) : mul_succ
+                 ... = n * succ l + m * succ l  : mul_succ)
 
-theorem mul.distr_left (n m k : ℕ) : n * (m + k) = n * m + n * k :=
+theorem mul.left_distrib (n m k : ℕ) : n * (m + k) = n * m + n * k :=
 calc
   n * (m + k) = (m + k) * n    : mul.comm
-          ... = m * n + k * n  : mul.distr_right
+          ... = m * n + k * n  : mul.right_distrib
           ... = n * m + k * n  : mul.comm
           ... = n * m + n * k  : mul.comm
 
 theorem mul.assoc (n m k : ℕ) : (n * m) * k = n * (m * k) :=
 induction_on k
   (calc
-    (n * m) * 0 = 0           : mul.zero_right
-            ... = n * 0       : mul.zero_right
-            ... = n * (m * 0) : mul.zero_right)
+    (n * m) * 0 = 0           : mul_zero
+            ... = n * 0       : mul_zero
+            ... = n * (m * 0) : mul_zero)
   (take l IH,
     calc
-      (n * m) * succ l = (n * m) * l + n * m : mul.succ_right
+      (n * m) * succ l = (n * m) * l + n * m : mul_succ
                    ... = n * (m * l) + n * m : IH
-                   ... = n * (m * l + m)     : mul.distr_left
-                   ... = n * (m * succ l)    : mul.succ_right)
+                   ... = n * (m * l + m)     : mul.left_distrib
+                   ... = n * (m * succ l)    : mul_succ)
 
 theorem mul.left_comm (n m k : ℕ) : n * (m * k) = m * (n * k) :=
 left_comm mul.comm mul.assoc n m k
@@ -292,32 +297,30 @@ left_comm mul.comm mul.assoc n m k
 theorem mul.right_comm (n m k : ℕ) : n * m * k = n * k * m :=
 right_comm mul.comm mul.assoc n m k
 
-theorem mul.one_right (n : ℕ) : n * 1 = n :=
+theorem mul.right_id (n : ℕ) : n * 1 = n :=
 calc
-  n * 1 = n * 0 + n : mul.succ_right
-    ... = 0 + n     : mul.zero_right
-    ... = n         : add.zero_left
+  n * 1 = n * 0 + n : mul_succ
+    ... = 0 + n     : mul_zero
+    ... = n         : add.left_id
 
-theorem mul.one_left (n : ℕ) : 1 * n = n :=
+theorem mul.left_id (n : ℕ) : 1 * n = n :=
 calc
   1 * n = n * 1 : mul.comm
-    ... = n     : mul.one_right
+    ... = n     : mul.right_id
 
-theorem mul.eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0 :=
-discriminate
-  (take Hn : n = 0, or.inl Hn)
-  (take (k : ℕ),
-    assume (Hk : n = succ k),
-    discriminate
-      (take (Hm : m = 0), or.inr Hm)
-      (take (l : ℕ),
-        assume (Hl : m = succ l),
-        have Heq : succ (k * succ l + l) = n * m, from
-         (calc
-            n * m = n * succ l            : Hl
-              ... = succ k * succ l       : Hk
-              ... = k * succ l + succ l   : mul.succ_left
-              ... = succ (k * succ l + l) : add.succ_right)⁻¹,
-        absurd (Heq ⬝ H) !succ_ne_zero))
+theorem eq_zero_or_eq_zero_of_mul_eq_zero {n m : ℕ} : n * m = 0 → n = 0 ∨ m = 0 :=
+cases_on n
+  (assume H, or.inl rfl)
+  (take n',
+    cases_on m
+      (assume H, or.inr rfl)
+      (take m',
+        assume H : succ n' * succ m' = 0,
+        absurd
+          ((calc
+            0 = succ n' * succ m' : H
+             ... = succ n' * m' + succ n' : mul_succ
+             ... = succ (succ n' * m' + n') : add_succ)⁻¹)
+          !succ_ne_zero))
 
 end nat
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 6ec381cc3..9d32f4e08 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -53,9 +53,9 @@ calc (x + z) div z
 
 theorem div_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y :=
 induction_on y
-  (calc (x + zero * z) div z = (x + zero) div z : mul.zero_left
-                       ...   = x div z          : add.zero_right
-                       ...   = x div z + zero   : add.zero_right)
+  (calc (x + zero * z) div z = (x + zero) div z : zero_mul
+                       ...   = x div z          : add.right_id
+                       ...   = x div z + zero   : add.right_id)
   (take y,
     assume IH : (x + y * z) div z = x div z + y, calc
       (x + succ y * z) div z = (x + y * z + z) div z    : by simp
@@ -93,12 +93,12 @@ calc (x + z) mod z
 
 theorem mod_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z :=
 induction_on y
-  (calc (x + zero * z) mod z = (x + zero) mod z : mul.zero_left
-                         ... = x mod z          : add.zero_right)
+  (calc (x + zero * z) mod z = (x + zero) mod z : zero_mul
+                         ... = x mod z          : add.right_id)
   (take y,
     assume IH : (x + y * z) mod z = x mod z,
     calc
-      (x + succ y * z) mod z = (x + (y * z + z)) mod z : mul.succ_left
+      (x + succ y * z) mod z = (x + (y * z + z)) mod z : succ_mul
                          ... = (x + y * z + z) mod z   : add.assoc
                          ... = (x + y * z) mod z       : mod_add_self_right H
                          ... = x mod z                 : IH)
@@ -139,8 +139,8 @@ theorem div_mod_eq {x y : ℕ} : x = x div y * y + x mod y :=
 case_zero_pos y
   (show x = x div 0 * 0 + x mod 0, from
     (calc
-      x div 0 * 0 + x mod 0 = 0 + x mod 0 : mul.zero_right
-        ... = x mod 0                     : add.zero_left
+      x div 0 * 0 + x mod 0 = 0 + x mod 0 : mul_zero
+        ... = x mod 0                     : add.left_id
         ... = x                           : mod_zero)⁻¹)
   (take y,
     assume H : y > 0,
@@ -163,7 +163,7 @@ case_zero_pos y
                 have H6 : succ x - y ≤ x, from lt_succ_imp_le H5,
                 (calc
                   succ x div y * y + succ x mod y = succ ((succ x - y) div y) * y + succ x mod y : H3
-                    ... = ((succ x - y) div y) * y + y + succ x mod y       : mul.succ_left
+                    ... = ((succ x - y) div y) * y + y + succ x mod y       : succ_mul
                     ... = ((succ x - y) div y) * y + y + (succ x - y) mod y : H4
                     ... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm
                     ... = succ x - y + y                                    : {!(IH _ H6)⁻¹}
@@ -202,7 +202,7 @@ by_cases -- (y = 0)
       (calc
         ((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq
           ... = z * (x div y * y + x mod y)                           : div_mod_eq
-          ... = z * (x div y * y) + z * (x mod y)                     : mul.distr_left
+          ... = z * (x div y * y) + z * (x mod y)                     : mul.left_distrib
           ... = (x div y) * (z * y) + z * (x mod y)                   : mul.left_comm))
 --- something wrong with the term order
 ---            ... = (x div y) * (z * y) + z * (x mod y) : by simp))
@@ -219,7 +219,7 @@ by_cases -- (y = 0)
       (calc
         ((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq
           ... = z * (x div y * y + x mod y)                           : div_mod_eq
-          ... = z * (x div y * y) + z * (x mod y)                     : mul.distr_left
+          ... = z * (x div y * y) + z * (x mod y)                     : mul.left_distrib
           ... = (x div y) * (z * y) + z * (x mod y)                   : mul.left_comm))
 
 theorem mod_one (x : ℕ) : x mod 1 = 0 :=
@@ -229,7 +229,7 @@ le_zero (lt_succ_imp_le H1)
 -- add_rewrite mod_one
 
 theorem mod_self (n : ℕ) : n mod n = 0 :=
-case n (by simp)
+cases_on n (by simp)
   (take n,
     have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
       from mod_mul_mul !succ_pos,
@@ -262,7 +262,7 @@ theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x :=
 (calc
   x = x div y * y + x mod y : div_mod_eq
     ... = x div y * y + 0 : {mp dvd_iff_mod_eq_zero H}
-    ... = x div y * y : !add.zero_right)⁻¹
+    ... = x div y * y : !add.right_id)⁻¹
 
 -- add_rewrite dvd_imp_div_mul_eq
 
@@ -281,7 +281,7 @@ show x mod y = 0, from
         calc
           x = z * y     : H
             ... = z * 0 : yz
-            ... = 0     : mul.zero_right,
+            ... = 0     : mul_zero,
       calc
         x mod y = x mod 0 : yz
           ... = x         : mod_zero
@@ -289,13 +289,13 @@ show x mod y = 0, from
     (assume ynz : y ≠ 0,
       have ypos : y > 0, from ne_zero_imp_pos ynz,
       have H3 : (z - x div y) * y < y, from H2⁻¹ ▸ mod_lt ypos,
-      have H4 : (z - x div y) * y < 1 * y, from !mul.one_left⁻¹ ▸ H3,
+      have H4 : (z - x div y) * y < 1 * y, from !mul.left_id⁻¹ ▸ H3,
       have H5 : z - x div y < 1, from mul_lt_cancel_right H4,
       have H6 : z - x div y = 0, from le_zero (lt_succ_imp_le H5),
       calc
         x mod y = (z - x div y) * y : H2
             ... = 0 * y             : H6
-            ... = 0                 : mul.zero_left)
+            ... = 0                 : zero_mul)
 
 theorem dvd_iff_exists_mul (x y : ℕ) : x | y ↔ ∃z, z * x = y :=
 iff.intro
@@ -345,7 +345,7 @@ mp (!dvd_iff_exists_mul⁻¹) (exists.intro (k div n * (n div m)) (H4⁻¹))
 
 theorem dvd_add {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 + n2) :=
 have H : (n1 div m + n2 div m) * m = n1 + n2, from calc
-  (n1 div m + n2 div m) * m = n1 div m * m + n2 div m * m : mul.distr_right
+  (n1 div m + n2 div m) * m = n1 div m * m + n2 div m * m : mul.right_distrib
                        ...  = n1 + n2 div m * m           : dvd_imp_div_mul_eq H1
                        ...  = n1 + n2                     : dvd_imp_div_mul_eq H2,
 mp (!dvd_iff_exists_mul⁻¹) (exists.intro _ H)
@@ -356,7 +356,7 @@ case_zero_pos m
     have H3 : n1 + n2 = 0, from (zero_dvd_eq (n1 + n2)) ▸ H1,
     have H4 : n1 = 0, from (zero_dvd_eq n1) ▸ H2,
     have H5 : n2 = 0, from calc
-      n2   = 0  + n2 : add.zero_left
+      n2   = 0  + n2 : add.left_id
        ... = n1 + n2 : H4
        ... = 0       : H3,
     show 0 | n2, from H5 ▸ dvd_self n2)
@@ -369,7 +369,7 @@ case_zero_pos m
           ... = (n1 div m * m + n2) div m * m : dvd_imp_div_mul_eq H2
           ... = (n2 + n1 div m * m) div m * m : add.comm
           ... = (n2 div m + n1 div m) * m     : div_add_mul_self_right mpos
-          ... = n2 div m * m + n1 div m * m   : mul.distr_right
+          ... = n2 div m * m + n1 div m * m   : mul.right_distrib
           ... = n1 div m * m + n2 div m * m   : add.comm
           ... = n1 + n2 div m * m             : dvd_imp_div_mul_eq H2,
     have H4 : n2 = n2 div m * m, from add.cancel_left H3,
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 41fcd72ab..62d2ca119 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -22,10 +22,10 @@ lt.step h
 theorem le.add_right (n k : ℕ) : n ≤ n + k :=
 induction_on k
   (calc n ≤ n        : le.refl n
-     ...  = n + zero : add.zero_right)
+     ...  = n + zero : add.right_id)
   (λ k (ih : n ≤ n + k), calc
      n   ≤ succ (n + k) : le.succ_right ih
-     ... = n + succ k   : add.succ_right)
+     ... = n + succ k   : add_succ)
 
 theorem le_intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
 h ▸ le.add_right n k
@@ -38,7 +38,7 @@ le.rec_on h
     (λ b hlt (ih : ∃ (k : ℕ), n + k = b),
       obtain (k : ℕ) (h : n + k = b), from ih,
       exists.intro (succ k) (calc
-        n + succ k = succ (n + k) : add.succ_right
+        n + succ k = succ (n + k) : add_succ
                ... = succ b       : h)))
 
 -- ### partial order (totality is part of less than)
@@ -47,11 +47,11 @@ theorem le_refl (n : ℕ) : n ≤ n :=
 le.refl n
 
 theorem zero_le (n : ℕ) : 0 ≤ n :=
-le_intro !add.zero_left
+le_intro !add.left_id
 
 theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
 obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
-add.eq_zero_left Hk
+eq_zero_of_add_eq_zero_right Hk
 
 theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0 :=
 (assume H : succ n ≤ 0,
@@ -70,10 +70,10 @@ have L1 : k + l = 0, from
       n + (k + l) = n + k + l : !add.assoc⁻¹
         ... = m + l           : {Hk}
         ... = n               : Hl
-        ... = n + 0           : !add.zero_right⁻¹),
-have L2 : k = 0, from add.eq_zero_left L1,
+        ... = n + 0           : !add.right_id⁻¹),
+have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
 calc
-  n = n + 0  : !add.zero_right⁻¹
+  n = n + 0  : !add.right_id⁻¹
 ... = n  + k : {L2⁻¹}
 ... = m      : Hk
 
@@ -120,13 +120,13 @@ show m ≤ l, from le_trans !le_add_left H4
 -- ### interaction with successor and predecessor
 
 theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
-!add.one ▸ !add.one ▸ add_le_right H 1
+!add_one ▸ !add_one ▸ add_le_right H 1
 
 theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) :  n ≤ m :=
-add_le_cancel_right (!add.one⁻¹ ▸ !add.one⁻¹ ▸ H)
+add_le_cancel_right (!add_one⁻¹ ▸ !add_one⁻¹ ▸ H)
 
 theorem self_le_succ (n : ℕ) : n ≤ succ n :=
-le_intro !add.one
+le_intro !add_one
 
 theorem le_imp_le_succ {n m : ℕ} (H : n ≤ m) : n ≤ succ m :=
 le_trans H !self_le_succ
@@ -137,7 +137,7 @@ discriminate
   (assume H3 : k = 0,
     have Heq : n = m,
       from calc
-        n = n + 0   : !add.zero_right⁻¹
+        n = n + 0   : !add.right_id⁻¹
         ... = n + k : {H3⁻¹}
         ... = m     : Hk,
     or.inr Heq)
@@ -146,7 +146,7 @@ discriminate
     have Hlt : succ n ≤ m, from
       (le_intro
         (calc
-          succ n + l = n + succ l : !add.move_succ
+          succ n + l = n + succ l : !succ_add_eq_add_succ
                  ... = n + k      : {H3⁻¹}
                  ... = m          : Hk)),
     or.inl Hlt)
@@ -163,7 +163,7 @@ obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H),
  and.intro
   (have H3 : n + succ k = m,
     from calc
-      n + succ k = succ n + k : !add.move_succ⁻¹
+      n + succ k = succ n + k : !succ_add_eq_add_succ⁻¹
              ... = m          : H2,
     show n ≤ m, from le_intro H3)
   (assume H3 : n = m,
@@ -172,7 +172,7 @@ obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H),
       show false, from absurd H5 succ.ne_self)
 
 theorem le_pred_self (n : ℕ) : pred n ≤ n :=
-case n
+cases_on n
   (pred.zero⁻¹ ▸ !le_refl)
   (take k : ℕ, !pred.succ⁻¹ ▸ !self_le_succ)
 
@@ -220,7 +220,7 @@ theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m :=
 obtain (l : ℕ) (Hl : n + l = m), from (le_elim H),
 have H2 : k * n + k * l = k * m, from
   calc
-    k * n + k * l = k * (n + l) : mul.distr_left
+    k * n + k * l = k * (n + l) : mul.left_distrib
               ... = k * m       : {Hl},
 le_intro H2
 
@@ -240,7 +240,7 @@ theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m :=
 le_elim (succ_le_of_lt H)
 
 theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
-lt_intro !add.move_succ
+lt_intro !succ_add_eq_add_succ
 
 -- ### basic facts
 
@@ -259,7 +259,7 @@ theorem succ_pos (n : ℕ) : 0 < succ n :=
 !zero_lt_succ
 
 theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n :=
-(or_resolve_right (zero_or_succ_pred n) (ne.symm (lt_imp_ne H))⁻¹)
+(or_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (lt_imp_ne H))⁻¹)
 
 theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
 discriminate
@@ -299,7 +299,7 @@ lt.asymm H
 -- ### interaction with addition
 
 theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
-lt_of_succ_le (!add.succ_right ▸ add_le_left (succ_le_of_lt H) k)
+lt_of_succ_le (!add_succ ▸ add_le_left (succ_le_of_lt H) k)
 
 theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
 !add.comm ▸ !add.comm ▸ add_lt_left H k
@@ -314,7 +314,7 @@ theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l :=
 add_lt_le H1 (lt_imp_le H2)
 
 theorem add_lt_cancel_left {n m k : ℕ} (H : k + n < k + m) : n < m :=
-lt_of_succ_le (add_le_cancel_left (!add.succ_right⁻¹ ▸ (succ_le_of_lt H)))
+lt_of_succ_le (add_le_cancel_left (!add_succ⁻¹ ▸ (succ_le_of_lt H)))
 
 theorem add_lt_cancel_right {n m k : ℕ} (H : n + k < m + k) : n < m :=
 add_lt_cancel_left (!add.comm ▸ !add.comm ▸ H)
@@ -322,10 +322,10 @@ add_lt_cancel_left (!add.comm ▸ !add.comm ▸ H)
 -- ### interaction with successor (see also the interaction with le)
 
 theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m :=
-!add.one ▸ !add.one ▸ add_lt_right H 1
+!add_one ▸ !add_one ▸ add_lt_right H 1
 
 theorem succ_lt_cancel {n m : ℕ} (H : succ n < succ m) :  n < m :=
-add_lt_cancel_right (!add.one⁻¹ ▸ !add.one⁻¹ ▸ H)
+add_lt_cancel_right (!add_one⁻¹ ▸ !add_one⁻¹ ▸ H)
 
 theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m :=
 lt.step H
@@ -381,7 +381,7 @@ protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P
 strong_induction_on a (
   take n,
   show (∀m, m < n → P m) → P n, from
-    case n
+    cases_on n
        (assume H : (∀m, m < 0 → P m), show P 0, from H0)
        (take n,
          assume H : (∀m, m < succ n → P m),
@@ -396,7 +396,7 @@ strong_induction_on a (
 -- ### basic
 
 theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) : P y :=
-case y H0 (take y, H1 !succ_pos)
+cases_on y H0 (take y, H1 !succ_pos)
 
 theorem zero_or_pos {n : ℕ} : n = 0 ∨ n > 0 :=
 or_of_or_of_imp_left
@@ -416,7 +416,7 @@ theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l :=
 lt_imp_eq_succ H
 
 theorem add_pos_right {n k : ℕ} (H : k > 0) : n + k > n :=
-!add.zero_right ▸ add_lt_left H n
+!add.right_id ▸ add_lt_left H n
 
 theorem add_pos_left {n : ℕ} {k : ℕ} (H : k > 0) : k + n > n :=
 !add.comm ▸ add_pos_right H
@@ -429,8 +429,8 @@ obtain (l : ℕ) (Hl : m = succ l), from pos_imp_eq_succ Hm,
 succ_imp_pos (calc
   n * m = succ k * m            : {Hk}
     ... = succ k * succ l       : {Hl}
-    ... = succ k * l + succ k   : !mul.succ_right
-    ... = succ (succ k * l + k) : !add.succ_right)
+    ... = succ k * l + succ k   : !mul_succ
+    ... = succ (succ k * l + k) : !add_succ)
 
 theorem mul_pos_imp_pos_left {n m : ℕ} (H : n * m > 0) : n > 0 :=
 discriminate
@@ -438,7 +438,7 @@ discriminate
     have H3 : n * m = 0,
       from calc
         n * m = 0 * m : {H2}
-          ... = 0     : !mul.zero_left,
+          ... = 0     : !zero_mul,
     have H4 : 0 > 0, from H3 ▸ H,
     absurd H4 !lt_irrefl)
   (take l : nat,
@@ -452,7 +452,7 @@ mul_pos_imp_pos_left (!mul.comm ▸ H)
 
 theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m :=
 have H2 : k * n < k * n + k, from add_pos_right Hk,
-have H3 : k * n + k ≤ k * m, from !mul.succ_right ▸ mul_le_left (succ_le_of_lt H) k,
+have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_left (succ_le_of_lt H) k,
 lt.of_lt_of_le H2 H3
 
 theorem mul_lt_right {n m k : ℕ} (Hk : k > 0) (H : n < m)  : n * k < m * k :=
@@ -481,7 +481,7 @@ mul_lt_cancel_left (!mul.comm ▸ !mul.comm ▸ H)
 
 theorem mul_le_cancel_left {n m k : ℕ} (Hk : k > 0) (H : k * n ≤ k * m) : n ≤ m :=
 have H2 : k * n < k * m + k, from lt.of_le_of_lt H (add_pos_right Hk),
-have H3 : k * n < k * succ m, from !mul.succ_right⁻¹ ▸ H2,
+have H3 : k * n < k * succ m, from !mul_succ⁻¹ ▸ H2,
 have H4 : n < succ m, from mul_lt_cancel_left H3,
 show n ≤ m, from lt_succ_imp_le H4
 
@@ -514,7 +514,7 @@ or.elim le_or_gt
     show n = 1, from le_antisym H5 (succ_le_of_lt H3))
   (assume H5 : n > 1,
     have H6 : n * m ≥ 2 * 1, from mul_le (succ_le_of_lt H5) (succ_le_of_lt H4),
-    have H7 : 1 ≥ 2, from !mul.one_right ▸ H ▸ H6,
+    have H7 : 1 ≥ 2, from !mul.right_id ▸ H ▸ H6,
     absurd !self_lt_succ (le_imp_not_gt H7))
 
 theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 60830950a..ea96dfda9 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -44,13 +44,13 @@ induction_on n !sub_zero_right (take k IH, !sub_succ_succ ⬝ IH)
 theorem sub_add_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m :=
 induction_on k
   (calc
-    (n + 0) - (m + 0) = n - (m + 0) : {!add.zero_right}
-                  ... = n - m       : {!add.zero_right})
+    (n + 0) - (m + 0) = n - (m + 0) : {!add.right_id}
+                  ... = n - m       : {!add.right_id})
   (take l : nat,
     assume IH : (n + l) - (m + l) = n - m,
     calc
-      (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {!add.succ_right}
-                              ... = succ (n + l) - succ (m + l) : {!add.succ_right}
+      (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {!add_succ}
+                              ... = succ (n + l) - succ (m + l) : {!add_succ}
                               ... = (n + l) - (m + l)           : !sub_succ_succ
                               ... =  n - m                      : IH)
 
@@ -59,11 +59,11 @@ theorem sub_add_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
 
 theorem sub_add_left (n m : ℕ) : n + m - m = n :=
 induction_on m
-  (!add.zero_right⁻¹ ▸ !sub_zero_right)
+  (!add.right_id⁻¹ ▸ !sub_zero_right)
   (take k : ℕ,
     assume IH : n + k - k = n,
     calc
-      n + succ k - succ k = succ (n + k) - succ k : {!add.succ_right}
+      n + succ k - succ k = succ (n + k) - succ k : {!add_succ}
                       ... = n + k - k             : !sub_succ_succ
                       ... = n                     : IH)
 
@@ -75,19 +75,19 @@ theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) :=
 induction_on k
   (calc
     n - m - 0 = n - m        : !sub_zero_right
-          ... =  n - (m + 0) : {!add.zero_right⁻¹})
+          ... =  n - (m + 0) : {!add.right_id⁻¹})
   (take l : nat,
     assume IH : n - m - l = n - (m + l),
     calc
       n - m - succ l = pred (n - m - l)   : !sub_succ_right
                  ... = pred (n - (m + l)) : {IH}
                  ... = n - succ (m + l)   : !sub_succ_right⁻¹
-                 ... = n - (m + succ l)   : {!add.succ_right⁻¹})
+                 ... = n - (m + succ l)   : {!add_succ⁻¹})
 
 theorem succ_sub_sub (n m k : ℕ) : succ n - m - succ k = n - m - k :=
 calc
   succ n - m - succ k = succ n - (m + succ k) : !sub_sub
-                  ... = succ n - succ (m + k) : {!add.succ_right}
+                  ... = succ n - succ (m + k) : {!add_succ}
                   ... = n - (m + k)           : !sub_succ_succ
                   ... = n - m - k             : !sub_sub⁻¹
 
@@ -119,15 +119,15 @@ theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m :=
 induction_on n
   (calc
     pred 0 * m = 0 * m     : {pred.zero}
-           ... = 0         : !mul.zero_left
+           ... = 0         : !zero_mul
            ... = 0 - m     : !sub_zero_left⁻¹
-           ... = 0 * m - m : {!mul.zero_left⁻¹})
+           ... = 0 * m - m : {!zero_mul⁻¹})
   (take k : nat,
     assume IH : pred k * m = k * m - m,
     calc
       pred (succ k) * m = k * m          : {!pred.succ}
                     ... = k * m + m - m  : !sub_add_left⁻¹
-                    ... = succ k * m - m : {!mul.succ_left⁻¹})
+                    ... = succ k * m - m : {!succ_mul⁻¹})
 
 theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n :=
 calc n * pred m = pred m * n : !mul.comm
@@ -139,7 +139,7 @@ induction_on m
   (calc
     (n - 0) * k = n * k         : {!sub_zero_right}
             ... = n * k - 0     : !sub_zero_right⁻¹
-            ... = n * k - 0 * k : {!mul.zero_left⁻¹})
+            ... = n * k - 0 * k : {!zero_mul⁻¹})
   (take l : nat,
     assume IH : (n - l) * k = n * k - l * k,
     calc
@@ -147,7 +147,7 @@ induction_on m
                    ... = (n - l) * k - k      : !mul_pred_left
                    ... = n * k - l * k - k    : {IH}
                    ... = n * k - (l * k + k)  : !sub_sub
-                   ... = n * k - (succ l * k) : {!mul.succ_left⁻¹})
+                   ... = n * k - (succ l * k) : {!succ_mul⁻¹})
 
 theorem mul_sub_distr_left (n m k : ℕ) : n * (m - k) = n * m - n * k :=
 calc
@@ -184,7 +184,7 @@ sub_induction n m
   (take k,
     assume H : 0 ≤ k,
     calc
-      0 + (k - 0) = k - 0 : !add.zero_left
+      0 + (k - 0) = k - 0 : !add.left_id
               ... = k     : !sub_zero_right)
   (take k, assume H : succ k ≤ 0, absurd H !not_succ_zero_le)
   (take k l,
@@ -201,7 +201,7 @@ theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n :=
 theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n :=
 calc
   n + (m - n) = n + 0 : {le_imp_sub_eq_zero H}
-          ... = n     : !add.zero_right
+          ... = n     : !add.right_id
 
 theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m :=
 !add.comm ▸ add_sub_ge
@@ -242,7 +242,7 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
       assume IH : k ≤ m → n + m - k = n + (m - k),
       take H : succ k ≤ succ m,
       calc
-        n + succ m - succ k = succ (n + m) - succ k : {!add.succ_right}
+        n + succ m - succ k = succ (n + m) - succ k : {!add_succ}
                         ... = n + m - k             : !sub_succ_succ
                         ... = n + (m - k)           : IH (succ_le_cancel H)
                         ... = n + (succ m - succ k) : {!sub_succ_succ⁻¹}),
@@ -254,7 +254,7 @@ sub_split
   (take k : ℕ,
     assume H1 : m + k = n,
     assume H2 : k = 0,
-    have H3 : n = m, from !add.zero_right ▸ H2 ▸ H1⁻¹,
+    have H3 : n = m, from !add.right_id ▸ H2 ▸ H1⁻¹,
     H3 ▸ !le_refl)
 
 theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0)
@@ -308,7 +308,7 @@ sub_split
 
 theorem sub_pos_of_gt {m n : ℕ} (H : n > m) : n - m > 0 :=
 have H1 : n = n - m + m, from (add_sub_ge_left (lt_imp_le H))⁻¹,
-have H2 : 0 + m < n - m + m, from (add.zero_left m)⁻¹ ▸ H1 ▸ H,
+have H2 : 0 + m < n - m + m, from (add.left_id m)⁻¹ ▸ H1 ▸ H,
 !add_lt_cancel_right H2
 
 -- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m
@@ -321,14 +321,14 @@ have H2 : 0 + m < n - m + m, from (add.zero_left m)⁻¹ ▸ H1 ▸ H,
 
 theorem sub_triangle_inequality (n m k : ℕ) : n - k ≤ (n - m) + (m - k) :=
 sub_split
-  (assume H : n ≤ m, !add.zero_left⁻¹ ▸ sub_le_right H k)
+  (assume H : n ≤ m, !add.left_id⁻¹ ▸ sub_le_right H k)
   (take mn : ℕ,
     assume Hmn : m + mn = n,
     sub_split
       (assume H : m ≤ k,
         have H2 : n - k ≤ n - m, from sub_le_left H n,
         have H3 : n - k ≤ mn, from sub_intro Hmn ▸ H2,
-        show n - k ≤ mn + 0, from !add.zero_right⁻¹ ▸ H3)
+        show n - k ≤ mn + 0, from !add.right_id⁻¹ ▸ H3)
       (take km : ℕ,
         assume Hkm : k + km = m,
         have H : k + (mn + km) = n, from
@@ -363,16 +363,16 @@ calc
                 ... = 0           : rfl
 
 theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m :=
-have H2 : n - m = 0, from add.eq_zero_left H,
+have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H,
 have H3 : n ≤ m, from sub_eq_zero_imp_le H2,
-have H4 : m - n = 0, from add.eq_zero_right H,
+have H4 : m - n = 0, from eq_zero_of_add_eq_zero_left H,
 have H5 : m ≤ n, from sub_eq_zero_imp_le H4,
 le_antisym H3 H5
 
 theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n :=
 calc
   dist n m = 0 + (m - n) : {le_imp_sub_eq_zero H}
-       ... = m - n       : !add.zero_left
+       ... = m - n       : !add.left_id
 
 theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m :=
 !dist_comm ▸ dist_le H
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index 7e8a23728..7f54610b6 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -13,10 +13,10 @@ definition add (x y : nat)
 
 infixl `+` := add
 
-theorem add_zero_left (x : nat) : x + zero = x
+theorem add.left_id (x : nat) : x + zero = x
 := refl _
 
-theorem add_succ_left (x y : nat) : x + (succ y) = succ (x + y)
+theorem succ_add (x y : nat) : x + (succ y) = succ (x + y)
 := refl _
 
 definition is_zero (x : nat)
diff --git a/tests/lean/run/imp_curly.lean b/tests/lean/run/imp_curly.lean
index 53ab9a813..0ee790202 100644
--- a/tests/lean/run/imp_curly.lean
+++ b/tests/lean/run/imp_curly.lean
@@ -3,8 +3,8 @@ open nat
 
 theorem zero_left (n : ℕ) : 0 + n = n :=
 nat.induction_on n
-    !add.zero_right
+    !add.right_id
     (take m IH, show 0 + succ m = succ m, from
       calc
-        0 + succ m = succ (0 + m) : add.succ_right
+        0 + succ m = succ (0 + m) : add_succ
                ... = succ m       : IH)
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index 597e16759..1856def93 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -13,7 +13,7 @@ infixl `*` := mul
 
 axiom add_one (n:nat) : n + (succ zero) = succ n
 axiom mul_zero_right (n : nat) : n * zero = zero
-axiom add_zero_right (n : nat) : n + zero = n
+axiom add.right_id (n : nat) : n + zero = n
 axiom mul_succ_right (n m : nat) : n * succ m = n * m + n
 axiom add_assoc (n m k : nat) : (n + m) + k = n + (m + k)
 axiom add_right_comm (n m k : nat) : n + m + k = n + k + m
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 1d1d62509..1e406baa6 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -110,7 +110,7 @@ theorem length_concat (s t : list T) : length (s ++ t) = length s + length t :=
 list_induction_on s
   (calc
     length (concat nil t) = length t : refl _
-      ... = 0 + length t : {symm !add.zero_left}
+      ... = 0 + length t : {symm !add.left_id}
       ... = length (@nil T) + length t : refl _)
   (take x s,
     assume H : length (concat s t) = length s + length t,
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index 17e7514af..29641d5c8 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -132,59 +132,59 @@ theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
 -------------------------------------------------- add
 definition add (x y : ℕ) : ℕ := plus x y
 infixl `+` := add
-theorem add_zero_right (n : ℕ) : n + 0 = n
-theorem add_succ_right (n m : ℕ) : n + succ m = succ (n + m)
+theorem add.right_id (n : ℕ) : n + 0 = n
+theorem add_succ (n m : ℕ) : n + succ m = succ (n + m)
 ---------- comm, assoc
 
-theorem add_zero_left (n : ℕ) : 0 + n = n
+theorem add.left_id (n : ℕ) : 0 + n = n
 := induction_on n
-    (add_zero_right 0)
+    (add.right_id 0)
     (take m IH, show 0 + succ m = succ m, from
       calc
-        0 + succ m = succ (0 + m) : add_succ_right _ _
+        0 + succ m = succ (0 + m) : add_succ _ _
             ... = succ m : {IH})
 
-theorem add_succ_left (n m : ℕ) : (succ n) + m = succ (n + m)
+theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m)
 := induction_on m
     (calc
-      succ n + 0 = succ n : add_zero_right (succ n)
-        ... = succ (n + 0) : {symm (add_zero_right n)})
+      succ n + 0 = succ n : add.right_id (succ n)
+        ... = succ (n + 0) : {symm (add.right_id n)})
     (take k IH,
       calc
-        succ n + succ k = succ (succ n + k) : add_succ_right _ _
+        succ n + succ k = succ (succ n + k) : add_succ _ _
           ... = succ (succ (n + k)) : {IH}
-          ... = succ (n + succ k) : {symm (add_succ_right _ _)})
+          ... = succ (n + succ k) : {symm (add_succ _ _)})
 
 theorem add_comm (n m : ℕ) : n + m = m + n
 := induction_on m
-    (trans (add_zero_right _) (symm (add_zero_left _)))
+    (trans (add.right_id _) (symm (add.left_id _)))
     (take k IH,
       calc
-        n + succ k = succ (n+k) : add_succ_right _ _
+        n + succ k = succ (n+k) : add_succ _ _
           ... = succ (k + n) : {IH}
-          ... = succ k + n : symm (add_succ_left _ _))
+          ... = succ k + n : symm (succ_add _ _))
 
-theorem add_move_succ (n m : ℕ) : succ n + m = n + succ m
+theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m
 := calc
-    succ n + m = succ (n + m) : add_succ_left n m
-      ... = n +succ m : symm (add_succ_right n m)
+    succ n + m = succ (n + m) : succ_add n m
+      ... = n +succ m : symm (add_succ n m)
 
 theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n
 := calc
-    n + succ m = succ n + m : symm (add_move_succ n m)
+    n + succ m = succ n + m : symm (succ_add_eq_add_succ n m)
       ... = m + succ n : add_comm (succ n) m
 
 theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k)
 := induction_on k
     (calc
-      (n + m) + 0 = n + m : add_zero_right _
-        ... = n + (m + 0) : {symm (add_zero_right m)})
+      (n + m) + 0 = n + m : add.right_id _
+        ... = n + (m + 0) : {symm (add.right_id m)})
     (take l IH,
       calc
-        (n + m) + succ l = succ ((n + m) + l) : add_succ_right _ _
+        (n + m) + succ l = succ ((n + m) + l) : add_succ _ _
           ... = succ (n + (m + l)) : {IH}
-          ... = n + succ (m + l) : symm (add_succ_right _ _)
-          ... = n + (m + succ l) : {symm (add_succ_right _ _)})
+          ... = n + succ (m + l) : symm (add_succ _ _)
+          ... = n + (m + succ l) : {symm (add_succ _ _)})
 
 theorem add_left_comm (n m k : ℕ) : n + (m + k) = m + (n + k)
 := left_comm add_comm add_assoc n m k
@@ -200,15 +200,15 @@ theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k
   induction_on n
     (take H : 0 + m = 0 + k,
       calc
-        m = 0 + m : symm (add_zero_left m)
+        m = 0 + m : symm (add.left_id m)
           ... = 0 + k : H
-          ... = k : add_zero_left k)
+          ... = k : add.left_id k)
     (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
       have H2 : succ (n + m) = succ (n + k),
       from calc
-        succ (n + m) = succ n + m : symm (add_succ_left n m)
+        succ (n + m) = succ n + m : symm (succ_add n m)
           ... = succ n + k : H
-          ... = succ (n + k) : add_succ_left n k,
+          ... = succ (n + k) : succ_add n k,
       have H3 : n + m = n + k, from succ_inj H2,
       IH H3)
 
@@ -222,7 +222,7 @@ theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k
       ... = m + k : add_comm k m,
     add_cancel_left H2
 
-theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0
+theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0
 :=
   induction_on n
     (take (H : 0 + m = 0), refl 0)
@@ -231,15 +231,15 @@ theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0
       absurd
         (show succ (k + m) = 0, from
           calc
-            succ (k + m) = succ k + m : symm (add_succ_left k m)
+            succ (k + m) = succ k + m : symm (succ_add k m)
               ... = 0 : H)
         (succ_ne_zero (k + m)))
 
 theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0
-:= add_eq_zero_left (trans (add_comm m n) H)
+:= eq_zero_of_add_eq_zero_right (trans (add_comm m n) H)
 
 theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0
-:= and_intro (add_eq_zero_left H) (add_eq_zero_right H)
+:= and_intro (eq_zero_of_add_eq_zero_right H) (add_eq_zero_right H)
 
 -- add_eq_self below
 
@@ -248,14 +248,14 @@ theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0
 theorem add_one (n:ℕ) : n + 1 = succ n
 :=
   calc
-    n + 1 = succ (n + 0) : add_succ_right _ _
-      ... = succ n : {add_zero_right _}
+    n + 1 = succ (n + 0) : add_succ _ _
+      ... = succ n : {add.right_id _}
 
 theorem add_one_left (n:ℕ) : 1 + n = succ n
 :=
   calc
-    1 + n = succ (0 + n) : add_succ_left _ _
-      ... = succ n : {add_zero_left _}
+    1 + n = succ (0 + n) : succ_add _ _
+      ... = succ n : {add.left_id _}
 
 --the following theorem has a terrible name, but since the name is not a substring or superstring of another name, it is at least easy to globally replace it
 theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0)
@@ -278,7 +278,7 @@ theorem mul_zero_left (n:ℕ) : 0 * n = 0
     (take m IH,
       calc
         0 * succ m = 0 * m + 0 : mul_succ_right _ _
-          ... = 0 * m : add_zero_right _
+          ... = 0 * m : add.right_id _
           ... = 0 : IH)
 
 theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m
@@ -286,7 +286,7 @@ theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m
     (calc
       succ n * 0 = 0     : mul_zero_right _
         ... = n * 0      : symm (mul_zero_right _)
-        ... = n * 0 + 0  : symm (add_zero_right _))
+        ... = n * 0 + 0  : symm (add.right_id _))
     (take k IH,
       calc
         succ n * succ k = (succ n * k) + succ n : mul_succ_right _ _
@@ -309,7 +309,7 @@ theorem mul_add_distr_left (n m k : ℕ) : (n + m) * k = n * k + m * k
 := induction_on k
     (calc
       (n + m) * 0 = 0 : mul_zero_right _
-        ... = 0 + 0 : symm (add_zero_right _)
+        ... = 0 + 0 : symm (add.right_id _)
         ... = n * 0 + 0 : refl _
         ... = n * 0 + m * 0 : refl _)
     (take l IH, calc
@@ -351,7 +351,7 @@ theorem mul_one_right (n : ℕ) : n * 1 = n
 := calc
     n * 1 = n * 0 + n : mul_succ_right n 0
       ... = 0 + n : {mul_zero_right n}
-      ... = n : add_zero_left n
+      ... = n : add.left_id n
 
 theorem mul_one_left (n : ℕ) : 1 * n = n
 := calc
@@ -375,7 +375,7 @@ theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0
               n * m = n * succ l : { Hl }
                 ... = succ k * succ l : { Hk }
                 ... = k * succ l + succ l : mul_succ_left _ _
-                ... = succ (k * succ l + l) : add_succ_right _ _),
+                ... = succ (k * succ l + l) : add_succ _ _),
           absurd (trans Heq H) (succ_ne_zero _)))
 
 -- see more under "positivity" below
@@ -397,15 +397,15 @@ theorem le_intro2 (n m : ℕ) : n ≤ n + m
 := le_intro (refl (n + m))
 
 theorem le_refl (n : ℕ) : n ≤ n
-:= le_intro (add_zero_right n)
+:= le_intro (add.right_id n)
 
 theorem zero_le (n : ℕ) : 0 ≤ n
-:= le_intro (add_zero_left n)
+:= le_intro (add.left_id n)
 
 theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0
 :=
   obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
-  add_eq_zero_left Hk
+  eq_zero_of_add_eq_zero_right Hk
 
 theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0
 := assume H : succ n ≤ 0,
@@ -414,7 +414,7 @@ theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0
 
 theorem le_zero_inv {n : ℕ} (H : n ≤ 0) : n = 0
 := obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
-   add_eq_zero_left Hk
+   eq_zero_of_add_eq_zero_right Hk
 
 theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k
 := obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1,
@@ -434,10 +434,10 @@ theorem le_antisym {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m
          n + (k + l) = n + k + l : { symm (add_assoc n k l) }
            ... = m + l : { Hk }
            ... = n : Hl
-           ... = n + 0 : symm (add_zero_right n)),
-   have L2 : k = 0, from add_eq_zero_left L1,
+           ... = n + 0 : symm (add.right_id n)),
+   have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
    calc
-     n = n + 0 : symm (add_zero_right n)
+     n = n + 0 : symm (add.right_id n)
       ... = n  + k : { symm L2 }
       ... = m : Hk
 
@@ -487,7 +487,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
     (assume H3 : k = 0,
       have Heq : n = m,
         from calc
-          n = n + 0 : (add_zero_right n)⁻¹
+          n = n + 0 : (add.right_id n)⁻¹
             ... = n + k : {H3⁻¹}
             ... = m : Hk,
       or_intro_right _ Heq)
@@ -496,7 +496,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
       have Hlt : succ n ≤ m, from
         (le_intro
           (calc
-            succ n + l = n + succ l : add_move_succ n l
+            succ n + l = n + succ l : succ_add_eq_add_succ n l
               ... = n + k : {H3⁻¹}
               ... = m : Hk)),
       or_intro_left _ Hlt)
@@ -514,7 +514,7 @@ theorem succ_le_left_inv {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m
    and_intro
     (have H3 : n + succ k = m,
       from calc
-        n + succ k = succ n + k : symm (add_move_succ n k)
+        n + succ k = succ n + k : symm (succ_add_eq_add_succ n k)
           ... = m : H2,
       show n ≤ m, from le_intro H3)
     (assume H3 : n = m,
@@ -543,7 +543,7 @@ theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m
           pred n + l = pred (succ k) + l : {Hn}
             ... = k + l : {pred_succ k}
             ... = pred (succ (k + l)) : symm (pred_succ (k + l))
-            ... = pred (succ k + l) : {symm (add_succ_left k l)}
+            ... = pred (succ k + l) : {symm (succ_add k l)}
             ... = pred (n + l) : {symm Hn}
             ... = pred m : {Hl},
       le_intro H2)
@@ -574,7 +574,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
     (assume H3 : k = 0,
       have Heq : n = m,
         from calc
-          n = n + 0 : symm (add_zero_right n)
+          n = n + 0 : symm (add.right_id n)
             ... = n + k : {symm H3}
             ... = m : Hk,
       or_intro_right _ Heq)
@@ -583,7 +583,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
       have Hlt : succ n ≤ m, from
         (le_intro
           (calc
-            succ n + l = n + succ l : add_move_succ n l
+            succ n + l = n + succ l : succ_add_eq_add_succ n l
               ... = n + k : {symm H3}
               ... = m : Hk)),
       or_intro_left _ Hlt)
@@ -661,7 +661,7 @@ theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m
 := le_elim H
 
 theorem lt_intro2 (n m : ℕ) : n < n + succ m
-:= lt_intro (add_move_succ n m)
+:= lt_intro (succ_add_eq_add_succ n m)
 
 -------------------------------------------------- ge, gt
 
@@ -742,7 +742,7 @@ theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n
 ---------- interaction with add
 
 theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m
-:= add_succ_right k n ▸ add_le_left H k
+:= add_succ k n ▸ add_le_left H k
 
 theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k
 := add_comm k m ▸ add_comm k n ▸ add_lt_left H k
@@ -757,7 +757,7 @@ theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l
 := add_lt_le H1 (lt_imp_le H2)
 
 theorem add_lt_left_inv {n m k : ℕ} (H : k + n < k + m) : n < m
-:= add_le_left_inv (add_succ_right k n⁻¹ ▸ H)
+:= add_le_left_inv (add_succ k n⁻¹ ▸ H)
 
 theorem add_lt_right_inv {n m k : ℕ} (H : n + k < m + k) : n < m
 := add_lt_left_inv (add_comm m k ▸ add_comm n k ▸ H)
@@ -792,14 +792,14 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
                 from calc
                   m = k + l : symm Hl
                     ... = k + 0 : {H2}
-                    ... = k : add_zero_right k,
+                    ... = k : add.right_id k,
               have H4 : m < succ k, from subst  H3 (lt_self_succ m),
               or_intro_right _ H4)
             (take l2 : ℕ,
               assume H2 : l = succ l2,
               have H3 : succ k + l2 = m,
                 from calc
-                  succ k + l2 = k + succ l2 : add_move_succ k l2
+                  succ k + l2 = k + succ l2 : succ_add_eq_add_succ k l2
                     ... = k + l : {symm H2}
                     ... = m : Hl,
               or_intro_left _ (le_intro H3)))
@@ -857,7 +857,7 @@ theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0
       assume Hm : m = succ k,
       have H2 : succ n + k = n,
         from calc
-          succ n + k = n + succ k : add_move_succ n k
+          succ n + k = n + succ k : succ_add_eq_add_succ n k
             ... = n + m : {symm Hm}
             ... = n : H,
       have H3 : n < n, from lt_intro H2,
@@ -911,7 +911,7 @@ theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0
 := subst (symm H) (succ_pos m)
 
 theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
-:= subst (add_zero_right n) (add_lt_left H n)
+:= subst (add.right_id n) (add_lt_left H n)
 
 theorem add_pos_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n
 := subst (add_comm n k) (add_pos_right n H)
@@ -925,7 +925,7 @@ theorem mul_positive {n m : ℕ} (Hn : n > 0) (Hm : m > 0) : n * m > 0
      n * m = succ k * m : {Hk}
        ... = succ k * succ l : {Hl}
        ... = succ k * l + succ k : mul_succ_right (succ k) l
-       ... = succ (succ k * l + k) : add_succ_right _ _)
+       ... = succ (succ k * l + k) : add_succ _ _)
 
 theorem mul_positive_inv_left {n m : ℕ} (H : n * m > 0) : n > 0
 := discriminate
@@ -1100,13 +1100,13 @@ theorem sub_self (n : ℕ) : n - n = 0
 theorem sub_add_add_right (n m k : ℕ) : (n + k) - (m + k) = n - m
 := induction_on k
     (calc
-      (n + 0) - (m + 0) = n - (m + 0) : {add_zero_right _}
-        ... = n - m : {add_zero_right _})
+      (n + 0) - (m + 0) = n - (m + 0) : {add.right_id _}
+        ... = n - m : {add.right_id _})
     (take l : ℕ,
       assume IH : (n + l) - (m + l) = n - m,
       calc
-        (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ_right _ _}
-          ... = succ (n + l) - succ (m + l) : {add_succ_right _ _}
+        (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ _ _}
+          ... = succ (n + l) - succ (m + l) : {add_succ _ _}
           ... = (n + l) - (m + l) : sub_succ_succ _ _
           ... =  n - m : IH)
 
@@ -1115,11 +1115,11 @@ theorem sub_add_add_left (n m k : ℕ) : (k + n) - (k + m) = n - m
 
 theorem sub_add_left (n m : ℕ) : n + m - m = n
 := induction_on m
-    (subst (symm (add_zero_right n)) (sub_zero_right n))
+    (subst (symm (add.right_id n)) (sub_zero_right n))
     (take k : ℕ,
       assume IH : n + k - k = n,
       calc
-        n + succ k - succ k = succ (n + k) - succ k : {add_succ_right n k}
+        n + succ k - succ k = succ (n + k) - succ k : {add_succ n k}
           ... = n + k - k : sub_succ_succ _ _
           ... = n : IH)
 
@@ -1127,19 +1127,19 @@ theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k)
 := induction_on k
     (calc
       n - m - 0 = n - m : sub_zero_right _
-        ... =  n - (m + 0) : {symm (add_zero_right m)})
+        ... =  n - (m + 0) : {symm (add.right_id m)})
     (take l : ℕ,
       assume IH : n - m - l = n - (m + l),
       calc
         n - m - succ l = pred (n - m - l) : sub_succ_right (n - m) l
           ... = pred (n - (m + l)) : {IH}
           ... = n - succ (m + l) : symm (sub_succ_right n (m + l))
-          ... = n - (m + succ l) : {symm (add_succ_right m l)})
+          ... = n - (m + succ l) : {symm (add_succ m l)})
 
 theorem succ_sub_sub (n m k : ℕ) : succ n - m - succ k = n - m - k
 := calc
     succ n - m - succ k = succ n - (m + succ k) : sub_sub _ _ _
-      ... = succ n - succ (m + k) : {add_succ_right m k}
+      ... = succ n - succ (m + k) : {add_succ m k}
       ... = n - (m + k) : sub_succ_succ _ _
       ... = n - m - k : symm (sub_sub n m k)
 
@@ -1229,7 +1229,7 @@ theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m
     (take k,
       assume H : 0 ≤ k,
       calc
-        0 + (k - 0) = k - 0 : add_zero_left (k - 0)
+        0 + (k - 0) = k - 0 : add.left_id (k - 0)
           ... = k : sub_zero_right k)
     (take k, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k))
     (take k l,
@@ -1237,7 +1237,7 @@ theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m
       take H : succ k ≤ succ l,
       calc
         succ k + (succ l - succ k) = succ k + (l - k) : {sub_succ_succ l k}
-          ... = succ (k + (l - k)) : add_succ_left k (l - k)
+          ... = succ (k + (l - k)) : succ_add k (l - k)
           ... = succ l : {IH (succ_le_cancel H)})
 
 theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n
@@ -1246,7 +1246,7 @@ theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n
 theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n
 := calc
     n + (m - n) = n + 0 : {le_imp_sub_eq_zero H}
-      ... = n : add_zero_right n
+      ... = n : add.right_id n
 
 theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m
 := subst (add_comm m (n - m)) add_sub_ge
@@ -1294,7 +1294,7 @@ theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m -
         assume IH : k ≤ m → n + m - k = n + (m - k),
         take H : succ k ≤ succ m,
         calc
-          n + succ m - succ k = succ (n + m) - succ k : {add_succ_right n m}
+          n + succ m - succ k = succ (n + m) - succ k : {add_succ n m}
             ... = n + m - k : sub_succ_succ (n + m) k
             ... = n + (m - k) : IH (succ_le_cancel H)
             ... = n + (succ m - succ k) : {symm (sub_succ_succ m k)}),
@@ -1306,7 +1306,7 @@ theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m
     (take k : ℕ,
       assume H1 : m + k = n,
       assume H2 : k = 0,
-      have H3 : n = m, from subst (add_zero_right m) (subst H2 (symm H1)),
+      have H3 : n = m, from subst (add.right_id m) (subst H2 (symm H1)),
       subst H3 (le_refl n))
 
 theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0)
@@ -1362,7 +1362,7 @@ theorem dist_comm (n m : ℕ) : dist n m = dist m n
 
 theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m
 :=
-  have H2 : n - m = 0, from add_eq_zero_left H,
+  have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H,
   have H3 : n ≤ m, from sub_eq_zero_imp_le H2,
   have H4 : m - n = 0, from add_eq_zero_right H,
   have H5 : m ≤ n, from sub_eq_zero_imp_le H4,
@@ -1372,7 +1372,7 @@ theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n
 := calc
     dist n m = (n - m) + (m - n) : refl _
          ... = 0       + (m - n) : {le_imp_sub_eq_zero H}
-         ... = m - n             : add_zero_left (m - n)
+         ... = m - n             : add.left_id (m - n)
 
 theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m
 := subst (dist_comm m n) (dist_le H)
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 9e08e3e39..497c0978b 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -126,59 +126,59 @@ theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
 -------------------------------------------------- add
 definition add (x y : ℕ) : ℕ := plus x y
 infixl `+` := add
-theorem add_zero_right (n : ℕ) : n + 0 = n
-theorem add_succ_right (n m : ℕ) : n + succ m = succ (n + m)
+theorem add.right_id (n : ℕ) : n + 0 = n
+theorem add_succ (n m : ℕ) : n + succ m = succ (n + m)
 ---------- comm, assoc
 
-theorem add_zero_left (n : ℕ) : 0 + n = n
+theorem add.left_id (n : ℕ) : 0 + n = n
 := induction_on n
-    (add_zero_right 0)
+    (add.right_id 0)
     (take m IH, show 0 + succ m = succ m, from
       calc
-        0 + succ m = succ (0 + m) : add_succ_right _ _
+        0 + succ m = succ (0 + m) : add_succ _ _
             ... = succ m : {IH})
 
-theorem add_succ_left (n m : ℕ) : (succ n) + m = succ (n + m)
+theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m)
 := induction_on m
     (calc
-      succ n + 0 = succ n : add_zero_right (succ n)
-        ... = succ (n + 0) : {symm (add_zero_right n)})
+      succ n + 0 = succ n : add.right_id (succ n)
+        ... = succ (n + 0) : {symm (add.right_id n)})
     (take k IH,
       calc
-        succ n + succ k = succ (succ n + k) : add_succ_right _ _
+        succ n + succ k = succ (succ n + k) : add_succ _ _
           ... = succ (succ (n + k)) : {IH}
-          ... = succ (n + succ k) : {symm (add_succ_right _ _)})
+          ... = succ (n + succ k) : {symm (add_succ _ _)})
 
 theorem add_comm (n m : ℕ) : n + m = m + n
 := induction_on m
-    (trans (add_zero_right _) (symm (add_zero_left _)))
+    (trans (add.right_id _) (symm (add.left_id _)))
     (take k IH,
       calc
-        n + succ k = succ (n+k) : add_succ_right _ _
+        n + succ k = succ (n+k) : add_succ _ _
           ... = succ (k + n) : {IH}
-          ... = succ k + n : symm (add_succ_left _ _))
+          ... = succ k + n : symm (succ_add _ _))
 
-theorem add_move_succ (n m : ℕ) : succ n + m = n + succ m
+theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m
 := calc
-    succ n + m = succ (n + m) : add_succ_left n m
-      ... = n +succ m : symm (add_succ_right n m)
+    succ n + m = succ (n + m) : succ_add n m
+      ... = n +succ m : symm (add_succ n m)
 
 theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n
 := calc
-    n + succ m = succ n + m : symm (add_move_succ n m)
+    n + succ m = succ n + m : symm (succ_add_eq_add_succ n m)
       ... = m + succ n : add_comm (succ n) m
 
 theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k)
 := induction_on k
     (calc
-      (n + m) + 0 = n + m : add_zero_right _
-        ... = n + (m + 0) : {symm (add_zero_right m)})
+      (n + m) + 0 = n + m : add.right_id _
+        ... = n + (m + 0) : {symm (add.right_id m)})
     (take l IH,
       calc
-        (n + m) + succ l = succ ((n + m) + l) : add_succ_right _ _
+        (n + m) + succ l = succ ((n + m) + l) : add_succ _ _
           ... = succ (n + (m + l)) : {IH}
-          ... = n + succ (m + l) : symm (add_succ_right _ _)
-          ... = n + (m + succ l) : {symm (add_succ_right _ _)})
+          ... = n + succ (m + l) : symm (add_succ _ _)
+          ... = n + (m + succ l) : {symm (add_succ _ _)})
 
 theorem add_left_comm (n m k : ℕ) : n + (m + k) = m + (n + k)
 := left_comm add_comm add_assoc n m k
@@ -194,15 +194,15 @@ theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k
   induction_on n
     (take H : 0 + m = 0 + k,
       calc
-        m = 0 + m : symm (add_zero_left m)
+        m = 0 + m : symm (add.left_id m)
           ... = 0 + k : H
-          ... = k : add_zero_left k)
+          ... = k : add.left_id k)
     (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
       have H2 : succ (n + m) = succ (n + k),
       from calc
-        succ (n + m) = succ n + m : symm (add_succ_left n m)
+        succ (n + m) = succ n + m : symm (succ_add n m)
           ... = succ n + k : H
-          ... = succ (n + k) : add_succ_left n k,
+          ... = succ (n + k) : succ_add n k,
       have H3 : n + m = n + k, from succ_inj H2,
       IH H3)
 
@@ -216,7 +216,7 @@ theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k
       ... = m + k : add_comm k m,
     add_cancel_left H2
 
-theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0
+theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0
 :=
   induction_on n
     (take (H : 0 + m = 0), eq.refl 0)
@@ -225,15 +225,15 @@ theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0
       absurd
         (show succ (k + m) = 0, from
           calc
-            succ (k + m) = succ k + m : symm (add_succ_left k m)
+            succ (k + m) = succ k + m : symm (succ_add k m)
               ... = 0 : H)
         (succ_ne_zero (k + m)))
 
 theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0
-:= add_eq_zero_left (trans (add_comm m n) H)
+:= eq_zero_of_add_eq_zero_right (trans (add_comm m n) H)
 
 theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0
-:= and.intro (add_eq_zero_left H) (add_eq_zero_right H)
+:= and.intro (eq_zero_of_add_eq_zero_right H) (add_eq_zero_right H)
 
 -- add_eq_self below
 
@@ -242,14 +242,14 @@ theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0
 theorem add_one (n:ℕ) : n + 1 = succ n
 :=
   calc
-    n + 1 = succ (n + 0) : add_succ_right _ _
-      ... = succ n : {add_zero_right _}
+    n + 1 = succ (n + 0) : add_succ _ _
+      ... = succ n : {add.right_id _}
 
 theorem add_one_left (n:ℕ) : 1 + n = succ n
 :=
   calc
-    1 + n = succ (0 + n) : add_succ_left _ _
-      ... = succ n : {add_zero_left _}
+    1 + n = succ (0 + n) : succ_add _ _
+      ... = succ n : {add.left_id _}
 
 --the following theorem has a terrible name, but since the name is not a substring or superstring of another name, it is at least easy to globally replace it
 theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0)
@@ -272,7 +272,7 @@ theorem mul_zero_left (n:ℕ) : 0 * n = 0
     (take m IH,
       calc
         0 * succ m = 0 * m + 0 : mul_succ_right _ _
-          ... = 0 * m : add_zero_right _
+          ... = 0 * m : add.right_id _
           ... = 0 : IH)
 
 theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m
@@ -280,7 +280,7 @@ theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m
     (calc
       succ n * 0 = 0     : mul_zero_right _
         ... = n * 0      : symm (mul_zero_right _)
-        ... = n * 0 + 0  : symm (add_zero_right _))
+        ... = n * 0 + 0  : symm (add.right_id _))
     (take k IH,
       calc
         succ n * succ k = (succ n * k) + succ n : mul_succ_right _ _
@@ -303,7 +303,7 @@ theorem mul_add_distr_left (n m k : ℕ) : (n + m) * k = n * k + m * k
 := induction_on k
     (calc
       (n + m) * 0 = 0 : mul_zero_right _
-        ... = 0 + 0 : symm (add_zero_right _)
+        ... = 0 + 0 : symm (add.right_id _)
         ... = n * 0 + 0 : eq.refl _
         ... = n * 0 + m * 0 : eq.refl _)
     (take l IH, calc
@@ -345,7 +345,7 @@ theorem mul_one_right (n : ℕ) : n * 1 = n
 := calc
     n * 1 = n * 0 + n : mul_succ_right n 0
       ... = 0 + n : {mul_zero_right n}
-      ... = n : add_zero_left n
+      ... = n : add.left_id n
 
 theorem mul_one_left (n : ℕ) : 1 * n = n
 := calc
@@ -369,7 +369,7 @@ theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0
               n * m = n * succ l : { Hl }
                 ... = succ k * succ l : { Hk }
                 ... = k * succ l + succ l : mul_succ_left _ _
-                ... = succ (k * succ l + l) : add_succ_right _ _),
+                ... = succ (k * succ l + l) : add_succ _ _),
           absurd (trans Heq H) (succ_ne_zero _)))
 
 -- see more under "positivity" below
@@ -391,15 +391,15 @@ theorem le_intro2 (n m : ℕ) : n ≤ n + m
 := le_intro (eq.refl (n + m))
 
 theorem le_refl (n : ℕ) : n ≤ n
-:= le_intro (add_zero_right n)
+:= le_intro (add.right_id n)
 
 theorem zero_le (n : ℕ) : 0 ≤ n
-:= le_intro (add_zero_left n)
+:= le_intro (add.left_id n)
 
 theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0
 :=
   obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
-  add_eq_zero_left Hk
+  eq_zero_of_add_eq_zero_right Hk
 
 theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0
 := assume H : succ n ≤ 0,
@@ -408,7 +408,7 @@ theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0
 
 theorem le_zero_inv {n : ℕ} (H : n ≤ 0) : n = 0
 := obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
-   add_eq_zero_left Hk
+   eq_zero_of_add_eq_zero_right Hk
 
 theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k
 := obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1,
@@ -428,10 +428,10 @@ theorem le_antisym {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m
          n + (k + l) = n + k + l : { symm (add_assoc n k l) }
            ... = m + l : { Hk }
            ... = n : Hl
-           ... = n + 0 : symm (add_zero_right n)),
-   have L2 : k = 0, from add_eq_zero_left L1,
+           ... = n + 0 : symm (add.right_id n)),
+   have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
    calc
-     n = n + 0 : symm (add_zero_right n)
+     n = n + 0 : symm (add.right_id n)
       ... = n  + k : { symm L2 }
       ... = m : Hk
 
@@ -481,7 +481,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
     (assume H3 : k = 0,
       have Heq : n = m,
         from calc
-          n = n + 0 : (add_zero_right n)⁻¹
+          n = n + 0 : (add.right_id n)⁻¹
             ... = n + k : {H3⁻¹}
             ... = m : Hk,
       or.intro_right _ Heq)
@@ -490,7 +490,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
       have Hlt : succ n ≤ m, from
         (le_intro
           (calc
-            succ n + l = n + succ l : add_move_succ n l
+            succ n + l = n + succ l : succ_add_eq_add_succ n l
               ... = n + k : {H3⁻¹}
               ... = m : Hk)),
       or.intro_left _ Hlt)
@@ -508,7 +508,7 @@ theorem succ_le_left_inv {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m
    and.intro
     (have H3 : n + succ k = m,
       from calc
-        n + succ k = succ n + k : symm (add_move_succ n k)
+        n + succ k = succ n + k : symm (succ_add_eq_add_succ n k)
           ... = m : H2,
       show n ≤ m, from le_intro H3)
     (assume H3 : n = m,
@@ -537,7 +537,7 @@ theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m
           pred n + l = pred (succ k) + l : {Hn}
             ... = k + l : {pred_succ k}
             ... = pred (succ (k + l)) : symm (pred_succ (k + l))
-            ... = pred (succ k + l) : {symm (add_succ_left k l)}
+            ... = pred (succ k + l) : {symm (succ_add k l)}
             ... = pred (n + l) : {symm Hn}
             ... = pred m : {Hl},
       le_intro H2)
@@ -568,7 +568,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
     (assume H3 : k = 0,
       have Heq : n = m,
         from calc
-          n = n + 0 : symm (add_zero_right n)
+          n = n + 0 : symm (add.right_id n)
             ... = n + k : {symm H3}
             ... = m : Hk,
       or.intro_right _ Heq)
@@ -577,7 +577,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
       have Hlt : succ n ≤ m, from
         (le_intro
           (calc
-            succ n + l = n + succ l : add_move_succ n l
+            succ n + l = n + succ l : succ_add_eq_add_succ n l
               ... = n + k : {symm H3}
               ... = m : Hk)),
       or.intro_left _ Hlt)
@@ -659,7 +659,7 @@ theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m
 := le_elim H
 
 theorem lt_intro2 (n m : ℕ) : n < n + succ m
-:= lt_intro (add_move_succ n m)
+:= lt_intro (succ_add_eq_add_succ n m)
 
 -------------------------------------------------- ge, gt
 
@@ -740,7 +740,7 @@ theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n
 ---------- interaction with add
 
 theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m
-:= add_succ_right k n ▸ add_le_left H k
+:= add_succ k n ▸ add_le_left H k
 
 theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k
 := add_comm k m ▸ add_comm k n ▸ add_lt_left H k
@@ -755,7 +755,7 @@ theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l
 := add_lt_le H1 (lt_imp_le H2)
 
 theorem add_lt_left_inv {n m k : ℕ} (H : k + n < k + m) : n < m
-:= add_le_left_inv (add_succ_right k n⁻¹ ▸ H)
+:= add_le_left_inv (add_succ k n⁻¹ ▸ H)
 
 theorem add_lt_right_inv {n m k : ℕ} (H : n + k < m + k) : n < m
 := add_lt_left_inv (add_comm m k ▸ add_comm n k ▸ H)
@@ -790,14 +790,14 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
                 from calc
                   m = k + l : symm Hl
                     ... = k + 0 : {H2}
-                    ... = k : add_zero_right k,
+                    ... = k : add.right_id k,
               have H4 : m < succ k, from subst  H3 (lt_self_succ m),
               or.intro_right _ H4)
             (take l2 : ℕ,
               assume H2 : l = succ l2,
               have H3 : succ k + l2 = m,
                 from calc
-                  succ k + l2 = k + succ l2 : add_move_succ k l2
+                  succ k + l2 = k + succ l2 : succ_add_eq_add_succ k l2
                     ... = k + l : {symm H2}
                     ... = m : Hl,
               or.intro_left _ (le_intro H3)))
@@ -855,7 +855,7 @@ theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0
       assume Hm : m = succ k,
       have H2 : succ n + k = n,
         from calc
-          succ n + k = n + succ k : add_move_succ n k
+          succ n + k = n + succ k : succ_add_eq_add_succ n k
             ... = n + m : {symm Hm}
             ... = n : H,
       have H3 : n < n, from lt_intro H2,
@@ -915,7 +915,7 @@ theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0
 := or.elim (zero_or_pos n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
 
 theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
-:= subst (add_zero_right n) (add_lt_left H n)
+:= subst (add.right_id n) (add_lt_left H n)
 
 theorem add_pos_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n
 := subst (add_comm n k) (add_pos_right n H)
@@ -929,7 +929,7 @@ theorem mul_positive {n m : ℕ} (Hn : n > 0) (Hm : m > 0) : n * m > 0
      n * m = succ k * m : {Hk}
        ... = succ k * succ l : {Hl}
        ... = succ k * l + succ k : mul_succ_right (succ k) l
-       ... = succ (succ k * l + k) : add_succ_right _ _)
+       ... = succ (succ k * l + k) : add_succ _ _)
 
 theorem mul_positive_inv_left {n m : ℕ} (H : n * m > 0) : n > 0
 := discriminate
@@ -1104,13 +1104,13 @@ theorem sub_self (n : ℕ) : n - n = 0
 theorem sub_add_add_right (n m k : ℕ) : (n + k) - (m + k) = n - m
 := induction_on k
     (calc
-      (n + 0) - (m + 0) = n - (m + 0) : {add_zero_right _}
-        ... = n - m : {add_zero_right _})
+      (n + 0) - (m + 0) = n - (m + 0) : {add.right_id _}
+        ... = n - m : {add.right_id _})
     (take l : ℕ,
       assume IH : (n + l) - (m + l) = n - m,
       calc
-        (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ_right _ _}
-          ... = succ (n + l) - succ (m + l) : {add_succ_right _ _}
+        (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ _ _}
+          ... = succ (n + l) - succ (m + l) : {add_succ _ _}
           ... = (n + l) - (m + l) : sub_succ_succ _ _
           ... =  n - m : IH)
 
@@ -1119,11 +1119,11 @@ theorem sub_add_add_left (n m k : ℕ) : (k + n) - (k + m) = n - m
 
 theorem sub_add_left (n m : ℕ) : n + m - m = n
 := induction_on m
-    (subst (symm (add_zero_right n)) (sub_zero_right n))
+    (subst (symm (add.right_id n)) (sub_zero_right n))
     (take k : ℕ,
       assume IH : n + k - k = n,
       calc
-        n + succ k - succ k = succ (n + k) - succ k : {add_succ_right n k}
+        n + succ k - succ k = succ (n + k) - succ k : {add_succ n k}
           ... = n + k - k : sub_succ_succ _ _
           ... = n : IH)
 
@@ -1131,19 +1131,19 @@ theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k)
 := induction_on k
     (calc
       n - m - 0 = n - m : sub_zero_right _
-        ... =  n - (m + 0) : {symm (add_zero_right m)})
+        ... =  n - (m + 0) : {symm (add.right_id m)})
     (take l : ℕ,
       assume IH : n - m - l = n - (m + l),
       calc
         n - m - succ l = pred (n - m - l) : sub_succ_right (n - m) l
           ... = pred (n - (m + l)) : {IH}
           ... = n - succ (m + l) : symm (sub_succ_right n (m + l))
-          ... = n - (m + succ l) : {symm (add_succ_right m l)})
+          ... = n - (m + succ l) : {symm (add_succ m l)})
 
 theorem succ_sub_sub (n m k : ℕ) : succ n - m - succ k = n - m - k
 := calc
     succ n - m - succ k = succ n - (m + succ k) : sub_sub _ _ _
-      ... = succ n - succ (m + k) : {add_succ_right m k}
+      ... = succ n - succ (m + k) : {add_succ m k}
       ... = n - (m + k) : sub_succ_succ _ _
       ... = n - m - k : symm (sub_sub n m k)
 
@@ -1233,7 +1233,7 @@ theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m
     (take k,
       assume H : 0 ≤ k,
       calc
-        0 + (k - 0) = k - 0 : add_zero_left (k - 0)
+        0 + (k - 0) = k - 0 : add.left_id (k - 0)
           ... = k : sub_zero_right k)
     (take k, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k))
     (take k l,
@@ -1241,7 +1241,7 @@ theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m
       take H : succ k ≤ succ l,
       calc
         succ k + (succ l - succ k) = succ k + (l - k) : {sub_succ_succ l k}
-          ... = succ (k + (l - k)) : add_succ_left k (l - k)
+          ... = succ (k + (l - k)) : succ_add k (l - k)
           ... = succ l : {IH (succ_le_cancel H)})
 
 theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n
@@ -1250,7 +1250,7 @@ theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n
 theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n
 := calc
     n + (m - n) = n + 0 : {le_imp_sub_eq_zero H}
-      ... = n : add_zero_right n
+      ... = n : add.right_id n
 
 theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m
 := subst (add_comm m (n - m)) add_sub_ge
@@ -1298,7 +1298,7 @@ theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m -
         assume IH : k ≤ m → n + m - k = n + (m - k),
         take H : succ k ≤ succ m,
         calc
-          n + succ m - succ k = succ (n + m) - succ k : {add_succ_right n m}
+          n + succ m - succ k = succ (n + m) - succ k : {add_succ n m}
             ... = n + m - k : sub_succ_succ (n + m) k
             ... = n + (m - k) : IH (succ_le_cancel H)
             ... = n + (succ m - succ k) : {symm (sub_succ_succ m k)}),
@@ -1310,7 +1310,7 @@ theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m
     (take k : ℕ,
       assume H1 : m + k = n,
       assume H2 : k = 0,
-      have H3 : n = m, from subst (add_zero_right m) (subst H2 (symm H1)),
+      have H3 : n = m, from subst (add.right_id m) (subst H2 (symm H1)),
       subst H3 (le_refl n))
 
 theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0)
@@ -1366,7 +1366,7 @@ theorem dist_comm (n m : ℕ) : dist n m = dist m n
 
 theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m
 :=
-  have H2 : n - m = 0, from add_eq_zero_left H,
+  have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H,
   have H3 : n ≤ m, from sub_eq_zero_imp_le H2,
   have H4 : m - n = 0, from add_eq_zero_right H,
   have H5 : m ≤ n, from sub_eq_zero_imp_le H4,
@@ -1376,7 +1376,7 @@ theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n
 := calc
     dist n m = (n - m) + (m - n) : eq.refl _
          ... = 0       + (m - n) : {le_imp_sub_eq_zero H}
-         ... = m - n             : add_zero_left (m - n)
+         ... = m - n             : add.left_id (m - n)
 
 theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m
 := subst (dist_comm m n) (dist_le H)