diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 009484f7c..b2fe50c71 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -119,11 +119,11 @@ theorem add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
 /- monoid -/
 
 structure monoid [class] (A : Type) extends semigroup A, has_one A :=
-(mul_left_id : ∀a, mul one a = a) (mul_right_id : ∀a, mul a one = a)
+(one_mul : ∀a, mul one a = a) (mul_one : ∀a, mul a one = a)
 
-theorem mul.left_id [s : monoid A] (a : A) : 1 * a = a := !monoid.mul_left_id
+theorem one_mul [s : monoid A] (a : A) : 1 * a = a := !monoid.one_mul
 
-theorem mul.right_id [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_right_id
+theorem mul_one [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_one
 
 structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
 
@@ -131,11 +131,11 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
 /- additive monoid -/
 
 structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
-(add_left_id : ∀a, add zero a = a) (add_right_id : ∀a, add a zero = a)
+(zero_add : ∀a, add zero a = a) (add_zero : ∀a, add a zero = a)
 
-theorem add.left_id [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.add_left_id
+theorem zero_add [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add
 
-theorem add.right_id [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_right_id
+theorem add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
 
 structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
 
@@ -145,7 +145,7 @@ structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semi
 structure group [class] (A : Type) extends monoid A, has_inv A :=
 (mul_left_inv : ∀a, mul (inv a) a = one)
 
--- Note: with more work, we could derive the axiom mul_left_id
+-- Note: with more work, we could derive the axiom one_mul
 
 section group
 
@@ -158,21 +158,21 @@ section group
   calc
     a⁻¹ * (a * b) = a⁻¹ * a * b : !mul.assoc⁻¹
       ... = 1 * b : mul.left_inv
-      ... = b : mul.left_id
+      ... = b : one_mul
 
   theorem inv_mul_cancel_right (a b : A) : a * b⁻¹ * b = a :=
   calc
     a * b⁻¹ * b = a * (b⁻¹ * b) : mul.assoc
       ... = a * 1 : mul.left_inv
-    ... = a : mul.right_id
+    ... = a : mul_one
 
   theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b :=
   calc
-    a⁻¹ = a⁻¹ * 1 : !mul.right_id⁻¹
+    a⁻¹ = a⁻¹ * 1 : !mul_one⁻¹
       ... = a⁻¹ * (a * b) : H
       ... = b : inv_mul_cancel_left
 
-  theorem inv_one : 1⁻¹ = 1 := inv_eq_of_mul_eq_one (mul.left_id 1)
+  theorem inv_one : 1⁻¹ = 1 := inv_eq_of_mul_eq_one (one_mul 1)
 
   theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a)
 
@@ -203,13 +203,13 @@ section group
   calc
     a * (a⁻¹ * b) = a * a⁻¹ * b : !mul.assoc⁻¹
       ... = 1 * b : mul.right_inv
-      ... = b : mul.left_id
+      ... = b : one_mul
 
   theorem mul_inv_cancel_right (a b : A) : a * b * b⁻¹ = a :=
   calc
     a * b * b⁻¹ = a * (b * b⁻¹) : mul.assoc
       ... = a * 1 : mul.right_inv
-      ... = a : mul.right_id
+      ... = a : mul_one
 
   theorem inv_mul_eq (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
   inv_eq_of_mul_eq_one
@@ -222,7 +222,7 @@ section group
   calc
     a = a * b⁻¹ * b : !inv_mul_cancel_right⁻¹
       ... = 1 * b : H
-      ... = b : mul.left_id
+      ... = b : one_mul
 
   -- TODO: better names for the next eight theorems? (Also for additive ones.)
   theorem eq_mul_inv_of_mul_eq {a b c : A} (H : a * b = c) : a = c * b⁻¹ :=
@@ -294,21 +294,21 @@ section add_group
   calc
     -a + (a + b) = -a + a + b : add.assoc
       ... = 0 + b : add.left_inv
-      ... = b : add.left_id
+      ... = b : zero_add
 
   theorem neg_add_cancel_right (a b : A) : a + -b + b = a :=
   calc
     a + -b + b = a + (-b + b) : add.assoc
       ... = a + 0 : add.left_inv
-      ... = a : add.right_id
+      ... = a : add_zero
 
   theorem neg_eq_of_add_eq_zero {a b : A} (H : a + b = 0) : -a = b :=
   calc
-    -a = -a + 0 : add.right_id
+    -a = -a + 0 : add_zero
       ... = -a + (a + b) : H
       ... = b : neg_add_cancel_left
 
-  theorem neg_zero : -0 = 0 := neg_eq_of_add_eq_zero (add.left_id 0)
+  theorem neg_zero : -0 = 0 := neg_eq_of_add_eq_zero (zero_add 0)
 
   theorem neg_neg (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a)
 
@@ -338,13 +338,13 @@ section add_group
   calc
     a + (-a + b) = a + -a + b : add.assoc
       ... = 0 + b : add.right_inv
-      ... = b : add.left_id
+      ... = b : zero_add
 
   theorem add_neg_cancel_right (a b : A) : a + b + -b = a :=
   calc
     a + b + -b = a + (b + -b) : add.assoc
       ... = a + 0 : add.right_inv
-      ... = a : add.right_id
+      ... = a : add_zero
 
   theorem neg_add_eq (a b : A) : -(a + b) = -b + -a :=
   neg_eq_of_add_eq_zero
@@ -420,14 +420,14 @@ section add_group
   calc
     a = (a - b) + b : !sub_add_cancel⁻¹
       ... = 0 + b : H
-      ... = b : add.left_id
+      ... = b : zero_add
 
   theorem eq_iff_sub_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
   iff.intro (assume H, H ▸ !sub_self) (assume H, eq_of_sub_eq_zero H)
 
-  theorem zero_sub_eq (a : A) : 0 - a = -a := !add.left_id
+  theorem zero_sub_eq (a : A) : 0 - a = -a := !zero_add
 
-  theorem sub_zero_eq (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add.right_id
+  theorem sub_zero_eq (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero
 
   theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg⁻¹ ▸ rfl
 
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 5790f4827..38f764cd0 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -88,28 +88,28 @@ section
 
   -- here we start using properties of zero.
   theorem add_nonneg {a b : A} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b :=
-  !add.left_id ▸ (add_le_add Ha Hb)
+  !zero_add ▸ (add_le_add Ha Hb)
 
   theorem add_pos_of_pos_of_nonneg {a b : A} (Ha : 0 < a) (Hb : 0 ≤ b) : 0 < a + b :=
-  !add.left_id ▸ (add_lt_add_of_lt_of_le Ha Hb)
+  !zero_add ▸ (add_lt_add_of_lt_of_le Ha Hb)
 
   theorem add_pos_of_nonneg_of_pos {a b : A} (Ha : 0 ≤ a) (Hb : 0 < b) : 0 < a + b :=
-  !add.left_id ▸ (add_lt_add_of_le_of_lt Ha Hb)
+  !zero_add ▸ (add_lt_add_of_le_of_lt Ha Hb)
 
   theorem add_pos_of_pos_of_pos {a b : A} (Ha : 0 < a) (Hb : 0 < b) : 0 < a + b :=
-  !add.left_id ▸ (add_lt_add_of_lt_of_lt Ha Hb)
+  !zero_add ▸ (add_lt_add_of_lt_of_lt Ha Hb)
 
   theorem add_nonpos {a b : A} (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 :=
-  !add.left_id ▸ (add_le_add Ha Hb)
+  !zero_add ▸ (add_le_add Ha Hb)
 
   theorem add_neg_of_neg_of_nonpos {a b : A} (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 :=
-  !add.left_id ▸ (add_lt_add_of_lt_of_le Ha Hb)
+  !zero_add ▸ (add_lt_add_of_lt_of_le Ha Hb)
 
   theorem add_neg_of_nonpos_of_neg {a b : A} (Ha : a ≤ 0) (Hb : b < 0) : a + b < 0 :=
-  !add.left_id ▸ (add_lt_add_of_le_of_lt Ha Hb)
+  !zero_add ▸ (add_lt_add_of_le_of_lt Ha Hb)
 
   theorem add_neg_of_neg_of_neg {a b : A} (Ha : a < 0) (Hb : b < 0) : a + b < 0 :=
-  !add.left_id ▸ (add_lt_add_of_lt_of_lt Ha Hb)
+  !zero_add ▸ (add_lt_add_of_lt_of_lt Ha Hb)
 
   -- TODO: add nonpos version (will be easier with simplifier)
   theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_noneng {a b : A}
@@ -118,67 +118,67 @@ section
     (assume Hab : a + b = 0,
       have Ha' : a ≤ 0, from
         calc
-          a = a + 0 : add.right_id
+          a = a + 0 : add_zero
             ... ≤ a + b : add_le_add_left Hb
             ... = 0 : Hab,
       have Haz : a = 0, from le.antisym Ha' Ha,
       have Hb' : b ≤ 0, from
         calc
-          b = 0 + b : add.left_id
+          b = 0 + b : zero_add
             ... ≤ a + b : add_le_add_right Ha
             ... = 0 : Hab,
       have Hbz : b = 0, from le.antisym Hb' Hb,
       and.intro Haz Hbz)
     (assume Hab : a = 0 ∧ b = 0,
-      (and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add.right_id 0))
+      (and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add_zero 0))
 
   theorem le_add_of_nonneg_of_le (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c :=
-  !add.left_id ▸ add_le_add Ha Hbc
+  !zero_add ▸ add_le_add Ha Hbc
 
   theorem le_add_of_le_of_nonneg (Hbc : b ≤ c) (Ha : 0 ≤ a) : b ≤ c + a :=
-  !add.right_id ▸ add_le_add Hbc Ha
+  !add_zero ▸ add_le_add Hbc Ha
 
   theorem lt_add_of_pos_of_le (Ha : 0 < a) (Hbc : b ≤ c) : b < a + c :=
-  !add.left_id ▸ add_lt_add_of_lt_of_le Ha Hbc
+  !zero_add ▸ add_lt_add_of_lt_of_le Ha Hbc
 
   theorem lt_add_of_le_of_pos (Hbc : b ≤ c) (Ha : 0 < a) : b < c + a :=
-  !add.right_id ▸ add_lt_add_of_le_of_lt Hbc Ha
+  !add_zero ▸ add_lt_add_of_le_of_lt Hbc Ha
 
   theorem add_le_of_nonpos_of_le (Ha : a ≤ 0) (Hbc : b ≤ c) : a + b ≤ c :=
-  !add.left_id ▸ add_le_add Ha Hbc
+  !zero_add ▸ add_le_add Ha Hbc
 
   theorem add_le_of_le_of_nonpos (Hbc : b ≤ c) (Ha : a ≤ 0) : b + a ≤ c :=
-  !add.right_id ▸ add_le_add Hbc Ha
+  !add_zero ▸ add_le_add Hbc Ha
 
   theorem add_lt_of_neg_of_le (Ha : a < 0) (Hbc : b ≤ c) : a + b < c :=
-  !add.left_id ▸ add_lt_add_of_lt_of_le Ha Hbc
+  !zero_add ▸ add_lt_add_of_lt_of_le Ha Hbc
 
   theorem add_lt_of_le_of_neg (Hbc : b ≤ c) (Ha : a < 0) : b + a < c :=
-  !add.right_id ▸ add_lt_add_of_le_of_lt Hbc Ha
+  !add_zero ▸ add_lt_add_of_le_of_lt Hbc Ha
 
   theorem lt_add_of_nonneg_of_lt (Ha : 0 ≤ a) (Hbc : b < c) : b < a + c :=
-  !add.left_id ▸ add_lt_add_of_le_of_lt Ha Hbc
+  !zero_add ▸ add_lt_add_of_le_of_lt Ha Hbc
 
   theorem lt_add_of_lt_of_nonneg (Hbc : b < c) (Ha : 0 ≤ a) : b < c + a :=
-  !add.right_id ▸ add_lt_add_of_lt_of_le Hbc Ha
+  !add_zero ▸ add_lt_add_of_lt_of_le Hbc Ha
 
   theorem lt_add_of_pos_of_lt (Ha : 0 < a) (Hbc : b < c) : b < a + c :=
-  !add.left_id ▸ add_lt_add_of_lt_of_lt Ha Hbc
+  !zero_add ▸ add_lt_add_of_lt_of_lt Ha Hbc
 
   theorem lt_add_of_lt_of_pos (Hbc : b < c) (Ha : 0 < a) : b < c + a :=
-  !add.right_id ▸ add_lt_add_of_lt_of_lt Hbc Ha
+  !add_zero ▸ add_lt_add_of_lt_of_lt Hbc Ha
 
   theorem add_lt_of_nonpos_of_lt (Ha : a ≤ 0) (Hbc : b < c) : a + b < c :=
-  !add.left_id ▸ add_lt_add_of_le_of_lt Ha Hbc
+  !zero_add ▸ add_lt_add_of_le_of_lt Ha Hbc
 
   theorem add_lt_of_lt_of_nonpos (Hbc : b < c) (Ha : a ≤ 0)  : b + a < c :=
-  !add.right_id ▸ add_lt_add_of_lt_of_le Hbc Ha
+  !add_zero ▸ add_lt_add_of_lt_of_le Hbc Ha
 
   theorem add_lt_of_neg_of_lt (Ha : a < 0) (Hbc : b < c) : a + b < c :=
-  !add.left_id ▸ add_lt_add_of_lt_of_lt Ha Hbc
+  !zero_add ▸ add_lt_add_of_lt_of_lt Ha Hbc
 
   theorem add_lt_of_lt_of_neg (Hbc : b < c) (Ha : a < 0) : b + a < c :=
-  !add.right_id ▸ add_lt_add_of_lt_of_lt Hbc Ha
+  !add_zero ▸ add_lt_add_of_lt_of_lt Hbc Ha
 
 end
 
@@ -194,7 +194,7 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_
 definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] (A : Type)
     [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
 ordered_cancel_comm_monoid.mk ordered_comm_group.add ordered_comm_group.add_assoc
-  (@ordered_comm_group.zero A s) add.left_id add.right_id ordered_comm_group.add_comm
+  (@ordered_comm_group.zero A s) zero_add add_zero ordered_comm_group.add_comm
   (@add.left_cancel _ _) (@add.right_cancel _ _)
   has_le.le le.refl (@le.trans _ _) (@le.antisym _ _)
   has_lt.lt (@lt_iff_le_and_ne _ _) ordered_comm_group.add_le_add_left
@@ -212,8 +212,8 @@ section
 
   theorem neg_le_neg_of_le {a b : A} (H : a ≤ b) : -b ≤ -a :=
   have H1 : 0 ≤ -a + b, from !add.left_inv ▸ !(add_le_add_left H),
-  !add_neg_cancel_right ▸ !add.left_id ▸ add_le_add_right H1 (-b)
---  !add.left_id ▸ !add_neg_cancel_right ▸ add_le_add_right H1 (-b)  -- doesn't work?
+  !add_neg_cancel_right ▸ !zero_add ▸ add_le_add_right H1 (-b)
+--  !zero_add ▸ !add_neg_cancel_right ▸ add_le_add_right H1 (-b)  -- doesn't work?
 
   theorem neg_le_neg_iff_le : -a ≤ -b ↔ b ≤ a :=
   iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_le_neg_of_le H) neg_le_neg_of_le
@@ -226,7 +226,7 @@ section
 
   theorem neg_lt_neg_of_lt {a b : A} (H : a < b) : -b < -a :=
   have H1 : 0 < -a + b, from !add.left_inv ▸ !(add_lt_add_left H),
-  !add_neg_cancel_right ▸ !add.left_id ▸ add_lt_add_right H1 (-b)
+  !add_neg_cancel_right ▸ !zero_add ▸ add_lt_add_right H1 (-b)
 
   theorem neg_lt_neg_iff_lt : -a < -b ↔ b < a :=
   iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_lt_neg_of_lt H) neg_lt_neg_of_lt
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index 38ee26ad0..be37dec55 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -155,8 +155,8 @@ structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A :
 
 definition ordered_ring.to_ordered_semiring [instance] [s : ordered_ring A] : ordered_semiring A :=
 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.zero_add ordered_ring.add_zero ordered_ring.add_comm ordered_ring.mul
+  ordered_ring.mul_assoc !ordered_ring.one ordered_ring.one_mul ordered_ring.mul_one
   ordered_ring.left_distrib ordered_ring.right_distrib
   zero_mul mul_zero !ordered_ring.zero_ne_one
   (@add.left_cancel A _) (@add.right_cancel A _)
@@ -263,15 +263,15 @@ section
     (assume H : a ≥ 0, mul_nonneg_of_nonneg_of_nonneg H H)
     (assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H)
 
-  theorem zero_le_one : 0 ≤ 1 := mul.left_id 1 ▸ mul_self_nonneg 1
+  theorem zero_le_one : 0 ≤ 1 := one_mul 1 ▸ mul_self_nonneg 1
 
   theorem zero_lt_one : 0 < 1 := lt_of_le_of_ne zero_le_one zero_ne_one
 
   -- TODO: move these to ordered_group.lean
-  theorem lt_add_of_pos_right {a b : A} (H : b > 0) : a < a + b := !add.right_id ▸ add_lt_add_left H a
-  theorem lt_add_of_pos_left {a b : A} (H : b > 0) : a < b + a := !add.left_id ▸ add_lt_add_right H a
-  theorem le_add_of_nonneg_right {a b : A} (H : b ≥ 0) : a ≤ a + b := !add.right_id ▸ add_le_add_left H a
-  theorem le_add_of_nonneg_left {a b : A} (H : b ≥ 0) : a ≤ b + a := !add.left_id ▸ add_le_add_right H a
+  theorem lt_add_of_pos_right {a b : A} (H : b > 0) : a < a + b := !add_zero ▸ add_lt_add_left H a
+  theorem lt_add_of_pos_left {a b : A} (H : b > 0) : a < b + a := !zero_add ▸ add_lt_add_right H a
+  theorem le_add_of_nonneg_right {a b : A} (H : b ≥ 0) : a ≤ a + b := !add_zero ▸ add_le_add_left H a
+  theorem le_add_of_nonneg_left {a b : A} (H : b ≥ 0) : a ≤ b + a := !zero_add ▸ add_le_add_right H a
 
   -- TODO: remove after we short-circuit class-graph
   definition linear_ordered_ring.to_mul [instance] [priority 100000] : has_mul A :=
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index b5b92aec9..dcb8b882a 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -86,7 +86,7 @@ section comm_semiring
   theorem dvd.elim {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, a * c = b → P) : P :=
   exists.elim H₁ H₂
 
-  theorem dvd.refl : a | a := dvd.intro (!mul.right_id)
+  theorem dvd.refl : a | a := dvd.intro !mul_one
 
   theorem dvd.trans {a b c : A} (H₁ : a | b) (H₂ : b | c) : a | c :=
   dvd.elim H₁
@@ -104,7 +104,7 @@ section comm_semiring
 
   theorem dvd_zero : a | 0 := dvd.intro !mul_zero
 
-  theorem one_dvd : 1 | a := dvd.intro !mul.left_id
+  theorem one_dvd : 1 | a := dvd.intro !one_mul
 
   theorem dvd_mul_right : a | a * b := dvd.intro rfl
 
@@ -156,22 +156,22 @@ end comm_semiring
 structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A, zero_ne_one_class A
 
 definition ring.to_semiring [instance] [s : ring A] : semiring A :=
-semiring.mk ring.add ring.add_assoc !ring.zero ring.add_left_id
-  add.right_id   -- note: we've shown that add_right_id follows from add_left_id in add_comm_group
-  ring.add_comm ring.mul ring.mul_assoc !ring.one ring.mul_left_id ring.mul_right_id
+semiring.mk ring.add ring.add_assoc !ring.zero ring.zero_add
+  add_zero   -- note: we've shown that add_zero follows from zero_add in add_comm_group
+  ring.add_comm ring.mul ring.mul_assoc !ring.one ring.one_mul ring.mul_one
   ring.left_distrib ring.right_distrib
   (take a,
     have H : 0 * a + 0 = 0 * a + 0 * a, from
       calc
-        0 * a + 0 = 0 * a : add.right_id
-          ... = (0 + 0) * a : {(add.right_id 0)⁻¹}
+        0 * a + 0 = 0 * a : add_zero
+          ... = (0 + 0) * a : {(add_zero 0)⁻¹}
           ... = 0 * a + 0 * a : ring.right_distrib,
     show 0 * a = 0, from  (add.left_cancel H)⁻¹)
   (take a,
     have H : a * 0 + 0 = a * 0 + a * 0, from
       calc
-        a * 0 + 0 = a * 0 : add.right_id
-          ... = a * (0 + 0) : {(add.right_id 0)⁻¹}
+        a * 0 + 0 = a * 0 : add_zero
+          ... = a * (0 + 0) : {(add_zero 0)⁻¹}
           ... = a * 0 + a * 0 : ring.left_distrib,
     show a * 0 = 0, from (add.left_cancel H)⁻¹)
   !ring.zero_ne_one
@@ -232,8 +232,8 @@ structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
 
 definition comm_ring.to_comm_semiring [instance] [s : comm_ring A] : comm_semiring A :=
 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.zero_add comm_ring.add_zero comm_ring.add_comm comm_ring.mul comm_ring.mul_assoc
+  (@comm_ring.one A s) comm_ring.one_mul comm_ring.mul_one comm_ring.left_distrib
   comm_ring.right_distrib zero_mul mul_zero (@comm_ring.zero_ne_one A s)
   comm_ring.mul_comm
 
@@ -246,7 +246,7 @@ section
   theorem mul_self_sub_mul_self_eq : a * a - b * b = (a + b) * (a - b) := sorry
 
   theorem mul_self_sub_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
-  mul.right_id 1 ▸ mul_self_sub_mul_self_eq a 1
+  mul_one 1 ▸ mul_self_sub_mul_self_eq a 1
 
 end
 
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index e4a1f1ba4..a132d11ac 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.left_id))
+          ... = 0 + m : zero_add))
   (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.left_id
+        0 + n = n : zero_add
           ... = 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.left_id ▸ H2)⁻¹ ▸ H1))
+        (!zero_add ▸ 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.left_id ▸ H2)⁻¹ ▸ H1)
+        (!zero_add ▸ 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' :=
@@ -392,9 +392,9 @@ begin
   apply H2
 end
 
-theorem add.right_id (a : ℤ) : a + 0 = a := cases_on a (take m, rfl) (take m', rfl)
+theorem add_zero (a : ℤ) : a + 0 = a := cases_on a (take m, rfl) (take m', rfl)
 
-theorem add.left_id (a : ℤ) : 0 + a = a := add.comm a 0 ▸ add.right_id a
+theorem zero_add (a : ℤ) : 0 + a = a := add.comm a 0 ▸ add_zero a
 
 /- negation -/
 
@@ -500,13 +500,13 @@ cases_on a
           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) : zero_mul
-            ... = (0 + succ m' * 0, succ m' * n) : nat.add.left_id
+            ... = (0 + succ m' * 0, succ m' * n) : nat.zero_add
             ... = 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') : nat.add.left_id
+            ... = (succ m' * succ n', 0 * succ n') : nat.zero_add
             ... = (succ m' * succ n', 0) : zero_mul
             ... = repr (mul (neg_succ_of_nat m') (neg_succ_of_nat n')) : rfl)⁻¹))
 
@@ -558,15 +558,15 @@ eq_of_repr_equiv_repr
       ... = pmul (repr a) (repr (b * c)) : repr_mul
       ... = repr (a * (b * c)) : repr_mul) ▸ !equiv.refl)
 
-theorem mul.right_id (a : ℤ) : a * 1 = a :=
+theorem mul_one (a : ℤ) : a * 1 = a :=
 eq_of_repr_equiv_repr (equiv_of_eq
   ((calc
     repr (a * 1) = pmul (repr a) (repr 1) : repr_mul
       ... = (pr1 (repr a), pr2 (repr a)) : by simp
       ... = repr a : prod.eta)))
 
-theorem mul.left_id (a : ℤ) : 1 * a = a :=
-mul.comm a 1 ▸ mul.right_id a
+theorem one_mul (a : ℤ) : 1 * a = a :=
+mul.comm a 1 ▸ mul_one a
 
 theorem mul.right_distrib (a b c : ℤ) : (a + b) * c = a * c + b * c :=
 eq_of_repr_equiv_repr
@@ -601,8 +601,8 @@ or_of_or_of_imp_of_imp H3
   (assume H : (nat_abs b) = nat.zero, nat_abs_eq_zero H)
 
 definition integral_domain : algebra.integral_domain int :=
-algebra.integral_domain.mk add add.assoc zero add.left_id add.right_id neg add.left_inv
-add.comm mul mul.assoc (of_num 1) mul.left_id mul.right_id mul.left_distrib mul.right_distrib
+algebra.integral_domain.mk add add.assoc zero zero_add add_zero neg add.left_inv
+add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
 zero_ne_one mul.comm @eq_zero_or_eq_zero_of_mul_eq_zero
 
 /-
@@ -745,7 +745,7 @@ context port_algebra
 end port_algebra
 
 -- TODO: declare appropriate rewrite rules
--- add_rewrite add_left_id add_right_id
+-- add_rewrite zero_add add_zero
 -- add_rewrite add_comm add.assoc add_left_comm
 -- add_rewrite sub_def add_inverse_right add_inverse_left
 -- add_rewrite neg_add_distr
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 88f5f569d..2efa3a06d 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -45,7 +45,7 @@ exists.intro n (!add.comm ▸ iff.mp' !add_eq_iff_eq_add_neg (H1⁻¹))
 -- ### partial order
 
 theorem le_refl (a : ℤ) : a ≤ a :=
-le_intro (add.right_id a)
+le_intro (add_zero a)
 
 theorem le_of_nat (n m : ℕ) : (of_nat n ≤ of_nat m) ↔ (n ≤ m) :=
 iff.intro
@@ -78,13 +78,13 @@ have H3 : a + of_nat (n + m) = a + 0, from
       ... = a + n + m : (add.assoc a n m)⁻¹
       ... = b + m : {Hn}
       ... = a : Hm
-      ... = a + 0 : (add.right_id a)⁻¹,
+      ... = a + 0 : (add_zero 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.eq_zero_of_add_eq_zero_right H5,
 show a = b, from
   calc
-    a = a + of_nat 0 : (add.right_id a)⁻¹
+    a = a + of_nat 0 : (add_zero a)⁻¹
       ... = a + n : {H6⁻¹}
       ... = b : Hn
 
@@ -132,7 +132,7 @@ discriminate
   (assume H2 : n = 0,
     have H3 : a = b, from
       calc
-        a = a + 0 : (add.right_id a)⁻¹
+        a = a + 0 : (add_zero a)⁻¹
           ... = a + n : {H2⁻¹}
           ... = b : Hn,
     or.inr H3)
@@ -188,7 +188,7 @@ theorem le_iff_sub_nonneg (a b : ℤ) : a ≤ b ↔ 0 ≤ b - a :=
 iff.intro
   (assume H, !sub_self ▸ sub_le_right H a)
   (assume H,
-     have H1 : a ≤ b - a + a, from add.left_id a ▸ add_le_right H a,
+     have H1 : a ≤ b - a + a, from zero_add a ▸ add_le_right H a,
      !neg_add_cancel_right ▸ H1)
 
 
@@ -418,7 +418,7 @@ or_resolve_right (le_or_gt a b) H
 
 theorem pos_imp_exists_nat {a : ℤ} (H : a ≥ 0) : ∃n : ℕ, a = n :=
 obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le_elim H,
-exists.intro n (Hn⁻¹ ⬝ add.left_id n)
+exists.intro n (Hn⁻¹ ⬝ zero_add n)
 
 theorem neg_imp_exists_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n :=
 have H2 : -a ≥ 0, from zero_le_neg H,
@@ -484,7 +484,7 @@ theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb : b ≤ 0) (Hc : c ≤
 le_trans (mul_le_right_nonpos Hb Hc) (mul_le_left_nonpos (le_trans Hc Ha) Hd)
 
 theorem mul_lt_left_pos {a b c : ℤ} (Ha : a > 0) (H : b < c) : a * b < a * c :=
-have H2 : a * b < a * b + a, from add.right_id (a * b) ▸ add_lt_left Ha (a * b),
+have H2 : a * b < a * b + a, from add_zero (a * b) ▸ add_lt_left Ha (a * b),
 have H3 : a * b + a ≤ a * c, from (by simp) ▸ mul_le_left_nonneg (lt_imp_le Ha) H,
 lt_le_trans H2 H3
 
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index c918f9ec1..ffe424fd1 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -49,7 +49,7 @@ 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.left_id⁻¹) (λx s H, !add.succ_left⁻¹ ▸ H ▸ rfl)
+induction_on s (!zero_add⁻¹) (λx s H, !add.succ_left⁻¹ ▸ H ▸ rfl)
 
 -- add_rewrite length_nil length_cons
 
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 32c606dd7..86a0e89cf 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -59,8 +59,6 @@ rfl
 theorem pred.succ (n : ℕ) : pred (succ n) = n :=
 rfl
 
-irreducible pred
-
 theorem eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
 induction_on n
   (or.inl rfl)
@@ -104,17 +102,15 @@ general m
 
 /- addition -/
 
-theorem add.right_id (n : ℕ) : n + 0 = n :=
+theorem add_zero (n : ℕ) : n + 0 = n :=
 rfl
 
 theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) :=
 rfl
 
-irreducible add
-
-theorem add.left_id (n : ℕ) : 0 + n = n :=
+theorem zero_add (n : ℕ) : 0 + n = n :=
 induction_on n
-    !add.right_id
+    !add_zero
     (take m IH, show 0 + succ m = succ m, from
       calc
         0 + succ m = succ (0 + m) : add_succ
@@ -122,7 +118,7 @@ induction_on n
 
 theorem add.succ_left (n m : ℕ) : (succ n) + m = succ (n + m) :=
 induction_on m
-    (!add.right_id ▸ !add.right_id)
+    (!add_zero ▸ !add_zero)
     (take k IH, calc
       succ n + succ k = succ (succ n + k)    : add_succ
                   ... = succ (succ (n + k))  : IH
@@ -130,7 +126,7 @@ induction_on m
 
 theorem add.comm (n m : ℕ) : n + m = m + n :=
 induction_on m
-    (!add.right_id ⬝ !add.left_id⁻¹)
+    (!add_zero ⬝ !zero_add⁻¹)
     (take k IH, calc
         n + succ k = succ (n+k)   : add_succ
                ... = succ (k + n) : IH
@@ -141,7 +137,7 @@ theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m :=
 
 theorem add.assoc (n m k : ℕ) : (n + m) + k = n + (m + k) :=
 induction_on k
-    (!add.right_id ▸ !add.right_id)
+    (!add_zero ▸ !add_zero)
     (take l IH,
       calc
         (n + m) + succ l = succ ((n + m) + l)  : add_succ
@@ -158,7 +154,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.left_id⁻¹ ⬝ H ⬝ !add.left_id)
+    !zero_add⁻¹ ⬝ H ⬝ !zero_add)
   (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
@@ -190,10 +186,10 @@ theorem add.eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 :=
 and.intro (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H)
 
 theorem add_one (n : ℕ) : n + 1 = succ n :=
-!add.right_id ▸ !add_succ
+!add_zero ▸ !add_succ
 
 theorem one_add (n : ℕ) : 1 + n = succ n :=
-!add.left_id ▸ !add.succ_left
+!zero_add ▸ !add.succ_left
 
 /- multiplication -/
 
@@ -203,18 +199,16 @@ rfl
 theorem mul_succ (n m : ℕ) : n * succ m = n * m + n :=
 rfl
 
-irreducible mul
-
 -- commutativity, distributivity, associativity, identity
 
 theorem zero_mul (n : ℕ) : 0 * n = 0 :=
 induction_on n
   !mul_zero
-  (take m IH, !mul_succ ⬝ !add.right_id ⬝ IH)
+  (take m IH, !mul_succ ⬝ !add_zero ⬝ IH)
 
 theorem succ_mul (n m : ℕ) : (succ n) * m = (n * m) + m :=
 induction_on m
-  (!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add.right_id⁻¹)
+  (!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add_zero⁻¹)
   (take k IH, calc
     succ n * succ k = succ n * k + succ n   : mul_succ
                 ... = n * k + k + succ n    : IH
@@ -236,7 +230,7 @@ theorem mul.right_distrib (n m k : ℕ) : (n + m) * k = n * k + m * k :=
 induction_on k
   (calc
     (n + m) * 0 = 0             : mul_zero
-            ... = 0 + 0         : add.right_id
+            ... = 0 + 0         : add_zero
             ... = n * 0 + 0     : mul_zero
             ... = n * 0 + m * 0 : mul_zero)
   (take l IH, calc
@@ -258,9 +252,7 @@ calc
 theorem mul.assoc (n m k : ℕ) : (n * m) * k = n * (m * k) :=
 induction_on k
   (calc
-    (n * m) * 0 = 0           : mul_zero
-            ... = n * 0       : mul_zero
-            ... = n * (m * 0) : mul_zero)
+    (n * m) * 0 = n * (m * 0) : mul_zero)
   (take l IH,
     calc
       (n * m) * succ l = (n * m) * l + n * m : mul_succ
@@ -268,16 +260,16 @@ induction_on k
                    ... = n * (m * l + m)     : mul.left_distrib
                    ... = n * (m * succ l)    : mul_succ)
 
-theorem mul.right_id (n : ℕ) : n * 1 = n :=
+theorem mul_one (n : ℕ) : n * 1 = n :=
 calc
   n * 1 = n * 0 + n : mul_succ
     ... = 0 + n     : mul_zero
-    ... = n         : add.left_id
+    ... = n         : zero_add
 
-theorem mul.left_id (n : ℕ) : 1 * n = n :=
+theorem one_mul (n : ℕ) : 1 * n = n :=
 calc
   1 * n = n * 1 : mul.comm
-    ... = n     : mul.right_id
+    ... = n     : mul_one
 
 theorem eq_zero_or_eq_zero_of_mul_eq_zero {n m : ℕ} : n * m = 0 → n = 0 ∨ m = 0 :=
 cases_on n
@@ -299,8 +291,8 @@ section port_algebra
   open algebra
 
   protected definition comm_semiring [instance] : algebra.comm_semiring nat :=
-  algebra.comm_semiring.mk add add.assoc zero add.left_id add.right_id add.comm
-  mul mul.assoc (succ zero) mul.left_id mul.right_id mul.left_distrib mul.right_distrib
+  algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm
+  mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
   zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
 
   theorem mul.left_comm : ∀a b c : ℕ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index cb4cd9c86..8b0dbe99e 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -55,8 +55,8 @@ 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 : zero_mul
-                       ...   = x div z          : add.right_id
-                       ...   = x div z + zero   : add.right_id)
+                       ...   = x div z          : add_zero
+                       ...   = x div z + zero   : add_zero)
   (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
@@ -95,7 +95,7 @@ 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 : zero_mul
-                         ... = x mod z          : add.right_id)
+                         ... = x mod z          : add_zero)
   (take y,
     assume IH : (x + y * z) mod z = x mod z,
     calc
@@ -141,7 +141,7 @@ 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
-        ... = x mod 0                     : add.left_id
+        ... = x mod 0                     : zero_add
         ... = x                           : mod_zero)⁻¹)
   (take y,
     assume H : y > 0,
@@ -264,7 +264,7 @@ theorem mod_eq_zero_imp_div_mul_eq {x y : ℕ} (H : x mod y = 0) : x div y * y =
 (calc
   x = x div y * y + x mod y : div_mod_eq
     ... = x div y * y + 0 : H
-    ... = x div y * y : !add.right_id)⁻¹
+    ... = x div y * y : !add_zero)⁻¹
 
 -- add_rewrite dvd_imp_div_mul_eq
 
@@ -291,7 +291,7 @@ 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.left_id⁻¹ ▸ H3,
+      have H4 : (z - x div y) * y < 1 * y, from !one_mul⁻¹ ▸ 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
@@ -323,7 +323,7 @@ case_zero_pos m
     have H3 : n1 + n2 = 0, from eq_zero_of_zero_dvd H1,
     have H4 : n1 = 0, from eq_zero_of_zero_dvd H2,
     have H5 : n2 = 0, from calc
-      n2   = 0  + n2 : add.left_id
+      n2   = 0  + n2 : zero_add
        ... = n1 + n2 : H4
        ... = 0       : H3,
     show 0 | n2, from H5 ▸ dvd.refl n2)
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 62d2ca119..8586c567e 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -22,7 +22,7 @@ lt.step h
 theorem le.add_right (n k : ℕ) : n ≤ n + k :=
 induction_on k
   (calc n ≤ n        : le.refl n
-     ...  = n + zero : add.right_id)
+     ...  = n + zero : add_zero)
   (λ k (ih : n ≤ n + k), calc
      n   ≤ succ (n + k) : le.succ_right ih
      ... = n + succ k   : add_succ)
@@ -47,7 +47,7 @@ theorem le_refl (n : ℕ) : n ≤ n :=
 le.refl n
 
 theorem zero_le (n : ℕ) : 0 ≤ n :=
-le_intro !add.left_id
+le_intro !zero_add
 
 theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
 obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
@@ -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.right_id⁻¹),
+        ... = n + 0           : !add_zero⁻¹),
 have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
 calc
-  n = n + 0  : !add.right_id⁻¹
+  n = n + 0  : !add_zero⁻¹
 ... = n  + k : {L2⁻¹}
 ... = m      : Hk
 
@@ -137,7 +137,7 @@ discriminate
   (assume H3 : k = 0,
     have Heq : n = m,
       from calc
-        n = n + 0   : !add.right_id⁻¹
+        n = n + 0   : !add_zero⁻¹
         ... = n + k : {H3⁻¹}
         ... = m     : Hk,
     or.inr Heq)
@@ -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.right_id ▸ add_lt_left H n
+!add_zero ▸ add_lt_left H n
 
 theorem add_pos_left {n : ℕ} {k : ℕ} (H : k > 0) : k + n > n :=
 !add.comm ▸ add_pos_right H
@@ -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.right_id ▸ H ▸ H6,
+    have H7 : 1 ≥ 2, from !mul_one ▸ 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 ea96dfda9..7d7e6cf27 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -44,8 +44,8 @@ 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.right_id}
-                  ... = n - m       : {!add.right_id})
+    (n + 0) - (m + 0) = n - (m + 0) : {!add_zero}
+                  ... = n - m       : {!add_zero})
   (take l : nat,
     assume IH : (n + l) - (m + l) = n - m,
     calc
@@ -59,7 +59,7 @@ 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.right_id⁻¹ ▸ !sub_zero_right)
+  (!add_zero⁻¹ ▸ !sub_zero_right)
   (take k : ℕ,
     assume IH : n + k - k = n,
     calc
@@ -75,7 +75,7 @@ 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.right_id⁻¹})
+          ... =  n - (m + 0) : {!add_zero⁻¹})
   (take l : nat,
     assume IH : n - m - l = n - (m + l),
     calc
@@ -184,7 +184,7 @@ sub_induction n m
   (take k,
     assume H : 0 ≤ k,
     calc
-      0 + (k - 0) = k - 0 : !add.left_id
+      0 + (k - 0) = k - 0 : !zero_add
               ... = 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.right_id
+          ... = n     : !add_zero
 
 theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m :=
 !add.comm ▸ add_sub_ge
@@ -254,7 +254,7 @@ sub_split
   (take k : ℕ,
     assume H1 : m + k = n,
     assume H2 : k = 0,
-    have H3 : n = m, from !add.right_id ▸ H2 ▸ H1⁻¹,
+    have H3 : n = m, from !add_zero ▸ 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.left_id m)⁻¹ ▸ H1 ▸ H,
+have H2 : 0 + m < n - m + m, from (zero_add 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.left_id m)⁻¹ ▸ H1 ▸ H,
 
 theorem sub_triangle_inequality (n m k : ℕ) : n - k ≤ (n - m) + (m - k) :=
 sub_split
-  (assume H : n ≤ m, !add.left_id⁻¹ ▸ sub_le_right H k)
+  (assume H : n ≤ m, !zero_add⁻¹ ▸ 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.right_id⁻¹ ▸ H3)
+        show n - k ≤ mn + 0, from !add_zero⁻¹ ▸ H3)
       (take km : ℕ,
         assume Hkm : k + km = m,
         have H : k + (mn + km) = n, from
@@ -372,7 +372,7 @@ 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.left_id
+       ... = m - n       : !zero_add
 
 theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m :=
 !dist_comm ▸ dist_le H
diff --git a/tests/lean/run/algebra3.lean b/tests/lean/run/algebra3.lean
index 7a184e21c..acfceba35 100644
--- a/tests/lean/run/algebra3.lean
+++ b/tests/lean/run/algebra3.lean
@@ -39,7 +39,7 @@ structure ring [class] (A : Type)
     assoc→add.assoc
     comm→add.comm
     one→zero
-    right_id→add.right_id
+    right_id→add_zero
     left_id→add.left_id
     inv→uminus
     is_inv→uminus_is_inv,
diff --git a/tests/lean/run/imp_curly.lean b/tests/lean/run/imp_curly.lean
index 0ee790202..008aebd1c 100644
--- a/tests/lean/run/imp_curly.lean
+++ b/tests/lean/run/imp_curly.lean
@@ -3,7 +3,7 @@ open nat
 
 theorem zero_left (n : ℕ) : 0 + n = n :=
 nat.induction_on n
-    !add.right_id
+    !add_zero
     (take m IH, show 0 + succ m = succ m, from
       calc
         0 + succ m = succ (0 + m) : add_succ
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index 1856def93..f5895d4f0 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.right_id (n : nat) : n + zero = n
+axiom add_zero (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 1e406baa6..fa390e1aa 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.left_id}
+      ... = 0 + length t : {symm !zero_add}
       ... = 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 29641d5c8..883f3b33a 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -132,13 +132,13 @@ theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
 -------------------------------------------------- add
 definition add (x y : ℕ) : ℕ := plus x y
 infixl `+` := add
-theorem add.right_id (n : ℕ) : n + 0 = n
+theorem add_zero (n : ℕ) : n + 0 = n
 theorem add_succ (n m : ℕ) : n + succ m = succ (n + m)
 ---------- comm, assoc
 
-theorem add.left_id (n : ℕ) : 0 + n = n
+theorem zero_add (n : ℕ) : 0 + n = n
 := induction_on n
-    (add.right_id 0)
+    (add_zero 0)
     (take m IH, show 0 + succ m = succ m, from
       calc
         0 + succ m = succ (0 + m) : add_succ _ _
@@ -147,8 +147,8 @@ theorem add.left_id (n : ℕ) : 0 + n = n
 theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m)
 := induction_on m
     (calc
-      succ n + 0 = succ n : add.right_id (succ n)
-        ... = succ (n + 0) : {symm (add.right_id n)})
+      succ n + 0 = succ n : add_zero (succ n)
+        ... = succ (n + 0) : {symm (add_zero n)})
     (take k IH,
       calc
         succ n + succ k = succ (succ n + k) : add_succ _ _
@@ -157,7 +157,7 @@ theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m)
 
 theorem add_comm (n m : ℕ) : n + m = m + n
 := induction_on m
-    (trans (add.right_id _) (symm (add.left_id _)))
+    (trans (add_zero _) (symm (zero_add _)))
     (take k IH,
       calc
         n + succ k = succ (n+k) : add_succ _ _
@@ -177,8 +177,8 @@ theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n
 theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k)
 := induction_on k
     (calc
-      (n + m) + 0 = n + m : add.right_id _
-        ... = n + (m + 0) : {symm (add.right_id m)})
+      (n + m) + 0 = n + m : add_zero _
+        ... = n + (m + 0) : {symm (add_zero m)})
     (take l IH,
       calc
         (n + m) + succ l = succ ((n + m) + l) : add_succ _ _
@@ -200,9 +200,9 @@ 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.left_id m)
+        m = 0 + m : symm (zero_add m)
           ... = 0 + k : H
-          ... = k : add.left_id k)
+          ... = k : zero_add 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
@@ -249,13 +249,13 @@ theorem add_one (n:ℕ) : n + 1 = succ n
 :=
   calc
     n + 1 = succ (n + 0) : add_succ _ _
-      ... = succ n : {add.right_id _}
+      ... = succ n : {add_zero _}
 
 theorem add_one_left (n:ℕ) : 1 + n = succ n
 :=
   calc
     1 + n = succ (0 + n) : succ_add _ _
-      ... = succ n : {add.left_id _}
+      ... = succ n : {zero_add _}
 
 --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.right_id _
+          ... = 0 * m : add_zero _
           ... = 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.right_id _))
+        ... = n * 0 + 0  : symm (add_zero _))
     (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.right_id _)
+        ... = 0 + 0 : symm (add_zero _)
         ... = 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.left_id n
+      ... = n : zero_add n
 
 theorem mul_one_left (n : ℕ) : 1 * n = n
 := calc
@@ -397,10 +397,10 @@ theorem le_intro2 (n m : ℕ) : n ≤ n + m
 := le_intro (refl (n + m))
 
 theorem le_refl (n : ℕ) : n ≤ n
-:= le_intro (add.right_id n)
+:= le_intro (add_zero n)
 
 theorem zero_le (n : ℕ) : 0 ≤ n
-:= le_intro (add.left_id n)
+:= le_intro (zero_add n)
 
 theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0
 :=
@@ -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.right_id n)),
+           ... = n + 0 : symm (add_zero n)),
    have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
    calc
-     n = n + 0 : symm (add.right_id n)
+     n = n + 0 : symm (add_zero 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.right_id n)⁻¹
+          n = n + 0 : (add_zero n)⁻¹
             ... = n + k : {H3⁻¹}
             ... = m : Hk,
       or_intro_right _ Heq)
@@ -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.right_id n)
+          n = n + 0 : symm (add_zero n)
             ... = n + k : {symm H3}
             ... = m : Hk,
       or_intro_right _ Heq)
@@ -792,7 +792,7 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
                 from calc
                   m = k + l : symm Hl
                     ... = k + 0 : {H2}
-                    ... = k : add.right_id k,
+                    ... = k : add_zero k,
               have H4 : m < succ k, from subst  H3 (lt_self_succ m),
               or_intro_right _ H4)
             (take l2 : ℕ,
@@ -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.right_id n) (add_lt_left H n)
+:= subst (add_zero 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)
@@ -1100,8 +1100,8 @@ 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.right_id _}
-        ... = n - m : {add.right_id _})
+      (n + 0) - (m + 0) = n - (m + 0) : {add_zero _}
+        ... = n - m : {add_zero _})
     (take l : ℕ,
       assume IH : (n + l) - (m + l) = n - m,
       calc
@@ -1115,7 +1115,7 @@ 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.right_id n)) (sub_zero_right n))
+    (subst (symm (add_zero n)) (sub_zero_right n))
     (take k : ℕ,
       assume IH : n + k - k = n,
       calc
@@ -1127,7 +1127,7 @@ 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.right_id m)})
+        ... =  n - (m + 0) : {symm (add_zero m)})
     (take l : ℕ,
       assume IH : n - m - l = n - (m + l),
       calc
@@ -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.left_id (k - 0)
+        0 + (k - 0) = k - 0 : zero_add (k - 0)
           ... = k : sub_zero_right k)
     (take k, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k))
     (take k l,
@@ -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.right_id n
+      ... = n : add_zero n
 
 theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m
 := subst (add_comm m (n - m)) add_sub_ge
@@ -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.right_id m) (subst H2 (symm H1)),
+      have H3 : n = m, from subst (add_zero 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)
@@ -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.left_id (m - n)
+         ... = m - n             : zero_add (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 497c0978b..07c200530 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -126,13 +126,13 @@ theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
 -------------------------------------------------- add
 definition add (x y : ℕ) : ℕ := plus x y
 infixl `+` := add
-theorem add.right_id (n : ℕ) : n + 0 = n
+theorem add_zero (n : ℕ) : n + 0 = n
 theorem add_succ (n m : ℕ) : n + succ m = succ (n + m)
 ---------- comm, assoc
 
-theorem add.left_id (n : ℕ) : 0 + n = n
+theorem zero_add (n : ℕ) : 0 + n = n
 := induction_on n
-    (add.right_id 0)
+    (add_zero 0)
     (take m IH, show 0 + succ m = succ m, from
       calc
         0 + succ m = succ (0 + m) : add_succ _ _
@@ -141,8 +141,8 @@ theorem add.left_id (n : ℕ) : 0 + n = n
 theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m)
 := induction_on m
     (calc
-      succ n + 0 = succ n : add.right_id (succ n)
-        ... = succ (n + 0) : {symm (add.right_id n)})
+      succ n + 0 = succ n : add_zero (succ n)
+        ... = succ (n + 0) : {symm (add_zero n)})
     (take k IH,
       calc
         succ n + succ k = succ (succ n + k) : add_succ _ _
@@ -151,7 +151,7 @@ theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m)
 
 theorem add_comm (n m : ℕ) : n + m = m + n
 := induction_on m
-    (trans (add.right_id _) (symm (add.left_id _)))
+    (trans (add_zero _) (symm (zero_add _)))
     (take k IH,
       calc
         n + succ k = succ (n+k) : add_succ _ _
@@ -171,8 +171,8 @@ theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n
 theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k)
 := induction_on k
     (calc
-      (n + m) + 0 = n + m : add.right_id _
-        ... = n + (m + 0) : {symm (add.right_id m)})
+      (n + m) + 0 = n + m : add_zero _
+        ... = n + (m + 0) : {symm (add_zero m)})
     (take l IH,
       calc
         (n + m) + succ l = succ ((n + m) + l) : add_succ _ _
@@ -194,9 +194,9 @@ 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.left_id m)
+        m = 0 + m : symm (zero_add m)
           ... = 0 + k : H
-          ... = k : add.left_id k)
+          ... = k : zero_add 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
@@ -243,13 +243,13 @@ theorem add_one (n:ℕ) : n + 1 = succ n
 :=
   calc
     n + 1 = succ (n + 0) : add_succ _ _
-      ... = succ n : {add.right_id _}
+      ... = succ n : {add_zero _}
 
 theorem add_one_left (n:ℕ) : 1 + n = succ n
 :=
   calc
     1 + n = succ (0 + n) : succ_add _ _
-      ... = succ n : {add.left_id _}
+      ... = succ n : {zero_add _}
 
 --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.right_id _
+          ... = 0 * m : add_zero _
           ... = 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.right_id _))
+        ... = n * 0 + 0  : symm (add_zero _))
     (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.right_id _)
+        ... = 0 + 0 : symm (add_zero _)
         ... = 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.left_id n
+      ... = n : zero_add n
 
 theorem mul_one_left (n : ℕ) : 1 * n = n
 := calc
@@ -391,10 +391,10 @@ theorem le_intro2 (n m : ℕ) : n ≤ n + m
 := le_intro (eq.refl (n + m))
 
 theorem le_refl (n : ℕ) : n ≤ n
-:= le_intro (add.right_id n)
+:= le_intro (add_zero n)
 
 theorem zero_le (n : ℕ) : 0 ≤ n
-:= le_intro (add.left_id n)
+:= le_intro (zero_add n)
 
 theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0
 :=
@@ -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.right_id n)),
+           ... = n + 0 : symm (add_zero n)),
    have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
    calc
-     n = n + 0 : symm (add.right_id n)
+     n = n + 0 : symm (add_zero 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.right_id n)⁻¹
+          n = n + 0 : (add_zero n)⁻¹
             ... = n + k : {H3⁻¹}
             ... = m : Hk,
       or.intro_right _ Heq)
@@ -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.right_id n)
+          n = n + 0 : symm (add_zero n)
             ... = n + k : {symm H3}
             ... = m : Hk,
       or.intro_right _ Heq)
@@ -790,7 +790,7 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
                 from calc
                   m = k + l : symm Hl
                     ... = k + 0 : {H2}
-                    ... = k : add.right_id k,
+                    ... = k : add_zero k,
               have H4 : m < succ k, from subst  H3 (lt_self_succ m),
               or.intro_right _ H4)
             (take l2 : ℕ,
@@ -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.right_id n) (add_lt_left H n)
+:= subst (add_zero 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)
@@ -1104,8 +1104,8 @@ 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.right_id _}
-        ... = n - m : {add.right_id _})
+      (n + 0) - (m + 0) = n - (m + 0) : {add_zero _}
+        ... = n - m : {add_zero _})
     (take l : ℕ,
       assume IH : (n + l) - (m + l) = n - m,
       calc
@@ -1119,7 +1119,7 @@ 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.right_id n)) (sub_zero_right n))
+    (subst (symm (add_zero n)) (sub_zero_right n))
     (take k : ℕ,
       assume IH : n + k - k = n,
       calc
@@ -1131,7 +1131,7 @@ 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.right_id m)})
+        ... =  n - (m + 0) : {symm (add_zero m)})
     (take l : ℕ,
       assume IH : n - m - l = n - (m + l),
       calc
@@ -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.left_id (k - 0)
+        0 + (k - 0) = k - 0 : zero_add (k - 0)
           ... = k : sub_zero_right k)
     (take k, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k))
     (take k l,
@@ -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.right_id n
+      ... = n : add_zero n
 
 theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m
 := subst (add_comm m (n - m)) add_sub_ge
@@ -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.right_id m) (subst H2 (symm H1)),
+      have H3 : n = m, from subst (add_zero 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)
@@ -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.left_id (m - n)
+         ... = m - n             : zero_add (m - n)
 
 theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m
 := subst (dist_comm m n) (dist_le H)