diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index b2fe50c71..c5fc4388c 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -255,7 +255,7 @@ section group
   theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ :=
   iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv
 
-  definition group.to_left_cancel_semigroup [instance] : left_cancel_semigroup A :=
+  definition group.to_left_cancel_semigroup [instance] [coercion] : left_cancel_semigroup A :=
   left_cancel_semigroup.mk (@group.mul A s) (@group.mul_assoc A s)
     (take a b c,
       assume H : a * b = a * c,
@@ -264,7 +264,7 @@ section group
           ... = a⁻¹ * (a * c) : H
           ... = c : inv_mul_cancel_left)
 
-  definition group.to_right_cancel_semigroup [instance] : right_cancel_semigroup A :=
+  definition group.to_right_cancel_semigroup [instance] [coercion] : right_cancel_semigroup A :=
   right_cancel_semigroup.mk (@group.mul A s) (@group.mul_assoc A s)
     (take a b c,
       assume H : a * b = c * b,
@@ -383,7 +383,7 @@ section add_group
   theorem add_eq_iff_eq_add_neg (a b c : A) : a + b = c ↔ a = c + -b :=
   iff.intro eq_add_neg_of_add_eq add_eq_of_eq_add_neg
 
-  definition add_group.to_left_cancel_semigroup [instance] :
+  definition add_group.to_left_cancel_semigroup [instance] [coercion] :
     add_left_cancel_semigroup A :=
   add_left_cancel_semigroup.mk add_group.add add_group.add_assoc
     (take a b c,
@@ -393,7 +393,7 @@ section add_group
           ... = -a + (a + c) : H
           ... = c : neg_add_cancel_left)
 
-  definition add_group.to_add_right_cancel_semigroup [instance] :
+  definition add_group.to_add_right_cancel_semigroup [instance] [coercion] :
     add_right_cancel_semigroup A :=
   add_right_cancel_semigroup.mk add_group.add add_group.add_assoc
     (take a b c,
diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index ea2cfb444..cbed02d94 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: algebra.order
 Author: Jeremy Avigad
 
-Various types of orders. We develop weak orders (<=) and strict orders (<) separately. We also
+Various types of orders. We develop weak orders "≤" and strict orders "<" separately. We also
 consider structures with both, where the two are related by
 
   x < y ↔ (x ≤ y ∧ x ≠ y)   (order_pair)
@@ -16,16 +16,12 @@ with both < and ≤ as needed.
 -/
 
 import logic.eq logic.connectives
-import data.unit data.sigma data.prod
-import algebra.function algebra.binary
-
 open eq eq.ops
 
 namespace algebra
 
 variable {A : Type}
 
-
 /- overloaded symbols -/
 
 structure has_le [class] (A : Type) :=
@@ -62,21 +58,24 @@ calc_trans le_of_le_of_eq
 calc_trans lt_of_eq_of_lt
 calc_trans lt_of_lt_of_eq
 
-
 /- weak orders -/
 
 structure weak_order [class] (A : Type) extends has_le A :=
 (le_refl : ∀a, le a a)
 (le_trans : ∀a b c, le a b → le b c → le a c)
-(le_antisym : ∀a b, le a b → le b a → a = b)
+(le_antisymm : ∀a b, le a b → le b a → a = b)
 
-theorem le.refl [s : weak_order A] (a : A) : a ≤ a := !weak_order.le_refl
+section
+  variable [s : weak_order A]
+  include s
 
-theorem le.trans [s : weak_order A] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
+  theorem le.refl (a : A) : a ≤ a := !weak_order.le_refl
 
-calc_trans le.trans
+  theorem le.trans {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
+  calc_trans le.trans
 
-theorem le.antisym [s : weak_order A] {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisym
+  theorem le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
+end
 
 structure linear_weak_order [class] (A : Type) extends weak_order A :=
 (le_total : ∀a b, le a b ∨ le b a)
@@ -84,22 +83,28 @@ structure linear_weak_order [class] (A : Type) extends weak_order A :=
 theorem le.total [s : linear_weak_order A] (a b : A) : a ≤ b ∨ b ≤ a :=
 !linear_weak_order.le_total
 
-
 /- strict orders -/
 
 structure strict_order [class] (A : Type) extends has_lt A :=
 (lt_irrefl : ∀a, ¬ lt a a)
 (lt_trans : ∀a b c, lt a b → lt b c → lt a c)
 
-theorem lt.irrefl [s : strict_order A] (a : A) : ¬ a < a := !strict_order.lt_irrefl
+section
+  variable [s : strict_order A]
+  include s
 
-theorem lt.trans [s : strict_order A] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
+  theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
 
-calc_trans lt.trans
+  theorem lt.trans {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
+  calc_trans lt.trans
 
-theorem lt.ne [s : strict_order A] {a b : A} : a < b → a ≠ b :=
-assume lt_ab : a < b, assume eq_ab : a = b, lt.irrefl a (eq_ab⁻¹ ▸ lt_ab)
+  theorem ne_of_lt {a b : A} : a < b → a ≠ b :=
+  assume lt_ab : a < b, assume eq_ab : a = b,
+  show false, from lt.irrefl b (eq_ab ▸ lt_ab)
 
+  theorem lt.asymm {a b : A} (H : a < b) : ¬ b < a :=
+  assume H1 : b < a, lt.irrefl _ (lt.trans H H1)
+end
 
 /- well-founded orders -/
 
@@ -123,7 +128,6 @@ structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
 (lt_iff_le_ne : ∀a b, lt a b ↔ (le a b ∧ a ≠ b))
 
 section
-
   variable [s : order_pair A]
   variables {a b c : A}
   include s
@@ -137,7 +141,7 @@ section
   theorem lt_of_le_of_ne (H1 : a ≤ b) (H2 : a ≠ b) : a < b :=
   iff.mp (iff.symm lt_iff_le_and_ne) (and.intro H1 H2)
 
-  definition order_pair.to_strict_order [instance] [s : order_pair A] : strict_order A :=
+  definition order_pair.to_strict_order [instance] [coercion] [s : order_pair A] : strict_order A :=
   strict_order.mk
     order_pair.lt
     (show ∀a, ¬ a < a, from
@@ -155,7 +159,7 @@ section
       have ne_ac : a ≠ c, from
         assume eq_ac : a = c,
         have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
-        have eq_ab : a = b, from le.antisym le_ab le_ba,
+        have eq_ab : a = b, from le.antisymm le_ab le_ba,
         have ne_ab : a ≠ b, from and.elim_right (iff.mp lt_iff_le_and_ne lt_ab),
         ne_ab eq_ab,
       show a < c, from lt_of_le_of_ne le_ac ne_ac)
@@ -167,8 +171,8 @@ section
   have ne_ac : a ≠ c, from
     assume eq_ac : a = c,
     have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
-    have eq_ab : a = b, from le.antisym (le_of_lt lt_ab) le_ba,
-    show false, from lt.ne lt_ab eq_ab,
+    have eq_ab : a = b, from le.antisymm (le_of_lt lt_ab) le_ba,
+    show false, from ne_of_lt lt_ab eq_ab,
   show a < c, from lt_of_le_of_ne le_ac ne_ac
 
   theorem lt_of_le_of_lt : a ≤ b → b < c → a < c :=
@@ -178,8 +182,8 @@ section
   have ne_ac : a ≠ c, from
     assume eq_ac : a = c,
     have le_cb : c ≤ b, from eq_ac ▸ le_ab,
-    have eq_bc : b = c, from le.antisym (le_of_lt lt_bc) le_cb,
-    show false, from lt.ne lt_bc eq_bc,
+    have eq_bc : b = c, from le.antisymm (le_of_lt lt_bc) le_cb,
+    show false, from ne_of_lt lt_bc eq_bc,
   show a < c, from lt_of_le_of_ne le_ac ne_ac
 
   calc_trans lt_of_lt_of_le
@@ -192,11 +196,6 @@ section
   theorem not_lt_of_le (H : a ≤ b) : ¬ b < a :=
   assume H1 : b < a,
   lt.irrefl _ (lt_of_le_of_lt H H1)
-
-  theorem not_lt_of_lt (H : a < b) : ¬ b < a :=
-  assume H1 : b < a,
-  lt.irrefl _ (lt.trans H1 H)
-
 end
 
 structure strong_order_pair [class] (A : Type) extends order_pair A :=
@@ -205,7 +204,7 @@ structure strong_order_pair [class] (A : Type) extends order_pair A :=
 theorem le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ∨ a = b :=
 !strong_order_pair.le_iff_lt_or_eq
 
-theorem le_imp_lt_or_eq [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ∨ a = b :=
+theorem lt_or_eq_of_le [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ∨ a = b :=
 iff.mp le_iff_lt_or_eq le_ab
 
 -- We can also construct a strong order pair by defining a strict order, and then defining
@@ -214,7 +213,7 @@ iff.mp le_iff_lt_or_eq le_ab
 structure strict_order_with_le [class] (A : Type) extends strict_order A, has_le A :=
 (le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
 
-definition strict_order_with_le.to_order_pair [instance] [s : strict_order_with_le A] :
+definition strict_order_with_le.to_order_pair [instance] [coercion] [s : strict_order_with_le A] :
   strong_order_pair A :=
 strong_order_pair.mk strict_order_with_le.le
   (take a,
@@ -248,57 +247,60 @@ strong_order_pair.mk strict_order_with_le.le
       (assume lt_ab : a < b,
         have le_ab : a ≤ b,
           from iff.elim_right !strict_order_with_le.le_iff_lt_or_eq (or.intro_left _ lt_ab),
-        show a ≤ b ∧ a ≠ b, from and.intro le_ab (lt.ne lt_ab))
+        show a ≤ b ∧ a ≠ b, from and.intro le_ab (ne_of_lt lt_ab))
       (assume H : a ≤ b ∧ a ≠ b,
         have H1 : a < b ∨ a = b,
           from iff.mp !strict_order_with_le.le_iff_lt_or_eq (and.elim_left H),
         show a < b, from or_resolve_left H1 (and.elim_right H)))
   strict_order_with_le.le_iff_lt_or_eq
 
-
 /- linear orders -/
 
 structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak_order A
 
-structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A :=
-(lt_or_eq_or_lt : ∀a b, lt a b ∨ a = b ∨ lt b a)
+structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A,
+    linear_weak_order A
 
 section
-
   variable [s : linear_strong_order_pair A]
   variables (a b c : A)
   include s
 
-  theorem lt_or_eq_or_lt : a < b ∨ a = b ∨ b < a := !linear_strong_order_pair.lt_or_eq_or_lt
+  theorem lt.trichotomy : a < b ∨ a = b ∨ b < a :=
+  or.elim (le.total a b)
+    (assume H : a ≤ b,
+      or.elim (iff.mp !le_iff_lt_or_eq H) (assume H1, or.inl H1) (assume H1, or.inr (or.inl H1)))
+    (assume H : b ≤ a,
+      or.elim (iff.mp !le_iff_lt_or_eq H)
+        (assume H1, or.inr (or.inr H1))
+        (assume H1, or.inr (or.inl (H1⁻¹))))
 
-  theorem lt_or_eq_or_lt_cases {a b : A} {P : Prop}
+  theorem lt.by_cases {a b : A} {P : Prop}
     (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
-  or.elim !lt_or_eq_or_lt (assume H, H1 H) (assume H, or.elim H (assume H', H2 H') (assume H', H3 H'))
+  or.elim !lt.trichotomy
+    (assume H, H1 H)
+    (assume H, or.elim H (assume H', H2 H') (assume H', H3 H'))
 
-  definition linear_strong_order_pair.to_linear_order_pair [instance] [s : linear_strong_order_pair A] :
-    linear_order_pair A :=
+  definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion]
+     [s : linear_strong_order_pair A] : linear_order_pair A :=
   linear_order_pair.mk linear_strong_order_pair.le linear_strong_order_pair.le_refl
-    linear_strong_order_pair.le_trans linear_strong_order_pair.le_antisym linear_strong_order_pair.lt
+    linear_strong_order_pair.le_trans linear_strong_order_pair.le_antisymm
+    linear_strong_order_pair.lt
     linear_strong_order_pair.lt_iff_le_ne
     (take a b : A,
-      lt_or_eq_or_lt_cases
+      lt.by_cases
         (assume H : a < b, or.inl (le_of_lt H))
         (assume H1 : a = b, or.inl (H1 ▸ !le.refl))
         (assume H1 : b < a, or.inr (le_of_lt H1)))
 
   definition le_of_not_lt {a b : A} (H : ¬ a < b) : b ≤ a :=
-  lt_or_eq_or_lt_cases (assume H', absurd H' H) (assume H', H' ▸ !le.refl) (assume H', le_of_lt H')
+  lt.by_cases (assume H', absurd H' H) (assume H', H' ▸ !le.refl) (assume H', le_of_lt H')
 
   definition lt_of_not_le {a b : A} (H : ¬ a ≤ b) : b < a :=
-  lt_or_eq_or_lt_cases
+  lt.by_cases
     (assume H', absurd (le_of_lt H') H)
     (assume H', absurd (H' ▸ !le.refl) H)
     (assume H', H')
-
 end
 
-
-
-
-
 end algebra
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 38f764cd0..644e4fe48 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -5,114 +5,125 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: algebra.ordered_group
 Authors: Jeremy Avigad
 
-Partially ordered additive groups. Modeled on Isabelle's library. The comments below indicate that
-we could refine the structures, though we would have to declare more inheritance paths.
+Partially ordered additive groups, modeled on Isabelle's library. We could refine the structures,
+but we would have to declare more inheritance paths.
 -/
 
 import logic.eq data.unit data.sigma data.prod
 import algebra.function algebra.binary
 import algebra.group algebra.order
-
 open eq eq.ops   -- note: ⁻¹ will be overloaded
 
 namespace algebra
 
 variable {A : Type}
 
+/- partially ordered monoids, such as the natural numbers -/
+
 structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid A,
   add_left_cancel_semigroup A, add_right_cancel_semigroup A, order_pair A :=
 (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b))
 (le_of_add_le_add_left : ∀a b c, le (add a b) (add a c) → le b c)
 
 section
-
-  variables [s : ordered_cancel_comm_monoid A] (a b c d e : A)
+  variables [s : ordered_cancel_comm_monoid A]
+  variables {a b c d e : A}
   include s
 
-  theorem add_le_add_left {a b : A} (H : a ≤ b) (c : A) : c + a ≤ c + b :=
+  theorem add_le_add_left (H : a ≤ b) (c : A) : c + a ≤ c + b :=
   !ordered_cancel_comm_monoid.add_le_add_left H c
 
-  theorem add_le_add_right {a b : A} (H : a ≤ b) (c : A) : a + c ≤ b + c :=
+  theorem add_le_add_right (H : a ≤ b) (c : A) : a + c ≤ b + c :=
   (add.comm c a) ▸ (add.comm c b) ▸ (add_le_add_left H c)
 
-  theorem add_le_add {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d :=
+  theorem add_le_add (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d :=
   le.trans (add_le_add_right Hab c) (add_le_add_left Hcd b)
 
-  theorem add_lt_add_left {a b : A} (H : a < b) (c : A) : c + a < c + b :=
+  theorem add_lt_add_left (H : a < b) (c : A) : c + a < c + b :=
   have H1 : c + a ≤ c + b, from add_le_add_left (le_of_lt H) c,
   have H2 : c + a ≠ c + b, from
     take H3 : c + a = c + b,
     have H4 : a = b, from add.left_cancel H3,
-    lt.ne H H4,
+    ne_of_lt H H4,
   lt_of_le_of_ne H1 H2
 
-  theorem add_lt_add_right {a b : A} (H : a < b) (c : A) : a + c < b + c :=
+  theorem add_lt_add_right (H : a < b) (c : A) : a + c < b + c :=
   (add.comm c a) ▸ (add.comm c b) ▸ (add_lt_add_left H c)
 
-  theorem add_lt_add_of_lt_of_lt {a b c d : A} (Hab : a < b) (Hcd : c < d) : a + c < b + d :=
+  theorem le_add_of_nonneg_right (H : b ≥ 0) : a ≤ a + b :=
+    !add_zero ▸ add_le_add_left H a
+
+  theorem le_add_of_nonneg_left (H : b ≥ 0) : a ≤ b + a :=
+    !zero_add ▸ add_le_add_right H a
+
+  theorem add_lt_add (Hab : a < b) (Hcd : c < d) : a + c < b + d :=
   lt.trans (add_lt_add_right Hab c) (add_lt_add_left Hcd b)
 
-  theorem add_lt_add_of_le_of_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d :=
+  theorem add_lt_add_of_le_of_lt (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d :=
   lt_of_le_of_lt (add_le_add_right Hab c) (add_lt_add_left Hcd b)
 
-  theorem add_lt_add_of_lt_of_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d :=
+  theorem add_lt_add_of_lt_of_le (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d :=
   lt_of_lt_of_le (add_lt_add_right Hab c) (add_le_add_left Hcd b)
 
+  theorem lt_add_of_pos_right (H : b > 0) : a < a + b := !add_zero ▸ add_lt_add_left H a
+
+  theorem lt_add_of_pos_left (H : b > 0) : a < b + a := !zero_add ▸ add_lt_add_right H a
+
   -- here we start using le_of_add_le_add_left.
-  theorem le_of_add_le_add_left {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
+  theorem le_of_add_le_add_left (H : a + b ≤ a + c) : b ≤ c :=
   !ordered_cancel_comm_monoid.le_of_add_le_add_left H
 
-  theorem le_of_add_le_add_right {a b c : A} (H : a + b ≤ c + b) : a ≤ c :=
+  theorem le_of_add_le_add_right (H : a + b ≤ c + b) : a ≤ c :=
   le_of_add_le_add_left ((add.comm a b) ▸ (add.comm c b) ▸ H)
 
-  theorem lt_of_add_lt_add_left {a b c : A} (H : a + b < a + c) : b < c :=
+  theorem lt_of_add_lt_add_left (H : a + b < a + c) : b < c :=
   have H1 : b ≤ c, from le_of_add_le_add_left (le_of_lt H),
   have H2 : b ≠ c, from
     assume H3 : b = c, lt.irrefl _ (H3 ▸ H),
   lt_of_le_of_ne H1 H2
 
-  theorem lt_of_add_lt_add_right {a b c : A} (H : a + b < c + b) : a < c :=
+  theorem lt_of_add_lt_add_right (H : a + b < c + b) : a < c :=
   lt_of_add_lt_add_left ((add.comm a b) ▸ (add.comm c b) ▸ H)
 
-  theorem add_le_add_left_iff : a + b ≤ a + c ↔ b ≤ c :=
+  theorem add_le_add_left_iff (a b c : A) : a + b ≤ a + c ↔ b ≤ c :=
   iff.intro le_of_add_le_add_left (assume H, add_le_add_left H _)
 
-  theorem add_le_add_right_iff : a + b ≤ c + b ↔ a ≤ c :=
+  theorem add_le_add_right_iff (a b c : A) : a + b ≤ c + b ↔ a ≤ c :=
   iff.intro le_of_add_le_add_right (assume H, add_le_add_right H _)
 
-  theorem add_lt_add_left_iff : a + b < a + c ↔ b < c :=
+  theorem add_lt_add_left_iff (a b c : A) : a + b < a + c ↔ b < c :=
   iff.intro lt_of_add_lt_add_left (assume H, add_lt_add_left H _)
 
-  theorem add_lt_add_right_iff : a + b < c + b ↔ a < c :=
+  theorem add_lt_add_right_iff (a b c : A) : a + b < c + b ↔ a < c :=
   iff.intro lt_of_add_lt_add_right (assume H, add_lt_add_right H _)
 
   -- here we start using properties of zero.
-  theorem add_nonneg {a b : A} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b :=
+  theorem add_nonneg (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b :=
   !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 :=
+  theorem add_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a + b :=
+  !zero_add ▸ (add_lt_add Ha Hb)
+
+  theorem add_pos_of_pos_of_nonneg (Ha : 0 < a) (Hb : 0 ≤ b) : 0 < a + b :=
   !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 :=
+  theorem add_pos_of_nonneg_of_pos (Ha : 0 ≤ a) (Hb : 0 < b) : 0 < a + b :=
   !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 :=
-  !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 :=
+  theorem add_nonpos (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 :=
   !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 :=
+  theorem add_neg (Ha : a < 0) (Hb : b < 0) : a + b < 0 :=
+  !zero_add ▸ (add_lt_add Ha Hb)
+
+  theorem add_neg_of_neg_of_nonpos (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 :=
   !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 :=
+  theorem add_neg_of_nonpos_of_neg (Ha : a ≤ 0) (Hb : b < 0) : a + b < 0 :=
   !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 :=
-  !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}
+  theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg
     (Ha : 0 ≤ a) (Hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
   iff.intro
     (assume Hab : a + b = 0,
@@ -121,13 +132,13 @@ section
           a = a + 0 : add_zero
             ... ≤ a + b : add_le_add_left Hb
             ... = 0 : Hab,
-      have Haz : a = 0, from le.antisym Ha' Ha,
+      have Haz : a = 0, from le.antisymm Ha' Ha,
       have Hb' : b ≤ 0, from
         calc
           b = 0 + b : zero_add
             ... ≤ a + b : add_le_add_right Ha
             ... = 0 : Hab,
-      have Hbz : b = 0, from le.antisym Hb' Hb,
+      have Hbz : b = 0, from le.antisymm Hb' Hb,
       and.intro Haz Hbz)
     (assume Hab : a = 0 ∧ b = 0,
       (and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add_zero 0))
@@ -163,10 +174,10 @@ section
   !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 :=
-  !zero_add ▸ add_lt_add_of_lt_of_lt Ha Hbc
+  !zero_add ▸ add_lt_add Ha Hbc
 
   theorem lt_add_of_lt_of_pos (Hbc : b < c) (Ha : 0 < a) : b < c + a :=
-  !add_zero ▸ add_lt_add_of_lt_of_lt Hbc Ha
+  !add_zero ▸ add_lt_add Hbc Ha
 
   theorem add_lt_of_nonpos_of_lt (Ha : a ≤ 0) (Hbc : b < c) : a + b < c :=
   !zero_add ▸ add_lt_add_of_le_of_lt Ha Hbc
@@ -175,28 +186,25 @@ section
   !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 :=
-  !zero_add ▸ add_lt_add_of_lt_of_lt Ha Hbc
+  !zero_add ▸ add_lt_add Ha Hbc
 
   theorem add_lt_of_lt_of_neg (Hbc : b < c) (Ha : a < 0) : b + a < c :=
-  !add_zero ▸ add_lt_add_of_lt_of_lt Hbc Ha
-
+  !add_zero ▸ add_lt_add Hbc Ha
 end
 
--- TODO: there is more we can do if we have max and min (in order.lean as well)
+-- TODO: add properties of max and min
 
--- TODO: there is more we can do if we assume a ≤ b ↔ ∃c. a + c = b.
--- This covers the natural numbers,
--- but it is not clear whether it provides any further useful generality.
+/- partially ordered groups -/
 
 structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair A :=
 (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b))
 
-definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] (A : Type)
+definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion]
     [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) 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_le.le le.refl (@le.trans _ _) (@le.antisymm _ _)
   has_lt.lt (@lt_iff_le_and_ne _ _) ordered_comm_group.add_le_add_left
 proof
   take a b c : A,
@@ -206,17 +214,16 @@ proof
 qed
 
 section
-
   variables [s : ordered_comm_group A] (a b c d e : A)
   include s
 
-  theorem neg_le_neg_of_le {a b : A} (H : a ≤ b) : -b ≤ -a :=
+  theorem neg_le_neg {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 ▸ !zero_add ▸ add_le_add_right H1 (-b)
---  !zero_add ▸ !add_neg_cancel_right ▸ add_le_add_right H1 (-b)  -- doesn't work?
+  --  !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
+  iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_le_neg H) neg_le_neg
 
   theorem neg_nonpos_iff_nonneg : -a ≤ 0 ↔ 0 ≤ a :=
   neg_zero ▸ neg_le_neg_iff_le a 0
@@ -224,12 +231,12 @@ section
   theorem neg_nonneg_iff_nonpos : 0 ≤ -a ↔ a ≤ 0 :=
   neg_zero ▸ neg_le_neg_iff_le 0 a
 
-  theorem neg_lt_neg_of_lt {a b : A} (H : a < b) : -b < -a :=
+  theorem neg_lt_neg {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 ▸ !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
+  iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_lt_neg H) neg_lt_neg
 
   theorem neg_neg_iff_pos : -a < 0 ↔ 0 < a :=
   neg_zero ▸ neg_lt_neg_iff_lt a 0
@@ -275,27 +282,32 @@ section
   have H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff),
   !add_neg_cancel_right ▸ H
 
-  theorem add_lt_add_iff_lt_neg_add : a + b < c ↔ b < -a + c :=
+  theorem add_lt_iff_lt_neg_add_left : a + b < c ↔ b < -a + c :=
   have H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_add_left_iff),
   !neg_add_cancel_left ▸ H
 
-  theorem add_lt_add_iff_lt_sub_left : a + b < c ↔ b < c - a :=
-  !add.comm ▸ !add_lt_add_iff_lt_neg_add
+  theorem add_lt_iff_lt_neg_add_right : a + b < c ↔ a < -b + c :=
+  !add.comm ▸ !add_lt_iff_lt_neg_add_left
+
+  theorem add_lt_iff_lt_sub_left : a + b < c ↔ b < c - a :=
+  !add.comm ▸ !add_lt_iff_lt_neg_add_left
 
   theorem add_lt_add_iff_lt_sub_right : a + b < c ↔ a < c - b :=
   have H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff),
   !add_neg_cancel_right ▸ H
 
-  theorem lt_add_iff_neg_add_lt_add : a < b + c ↔ -b + a < c :=
+  theorem lt_add_iff_neg_add_lt_left : a < b + c ↔ -b + a < c :=
   have H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_add_left_iff),
   !neg_add_cancel_left ▸ H
 
-  theorem lt_add_iff_sub_left_lt : a < b + c ↔ a - b < c :=
-  !add.comm ▸ !lt_add_iff_neg_add_lt_add
+  theorem lt_add_iff_neg_add_lt_right : a < b + c ↔ -c + a < b :=
+  !add.comm ▸ !lt_add_iff_neg_add_lt_left
 
-  theorem lt_add_iff_sub_right_lt : a < b + c ↔ a - c < b :=
-  have H: a < b + c ↔ a - c < b + c - c, from iff.symm (!add_lt_add_right_iff),
-  !add_neg_cancel_right ▸ H
+  theorem lt_add_iff_sub_lt_left : a < b + c ↔ a - b < c :=
+  !add.comm ▸ !lt_add_iff_neg_add_lt_left
+
+  theorem lt_add_iff_sub_lt_right : a < b + c ↔ a - c < b :=
+  !add.comm ▸ !lt_add_iff_sub_lt_left
 
   -- TODO: the Isabelle library has varations on a + b ≤ b ↔ a ≤ 0
 
@@ -312,31 +324,29 @@ section
       ... ↔ c < d : sub_neg_iff_lt c d
 
   theorem sub_le_sub_left {a b : A} (H : a ≤ b) (c : A) : c - b ≤ c - a :=
-  add_le_add_left (neg_le_neg_of_le H) c
+  add_le_add_left (neg_le_neg H) c
 
   theorem sub_le_sub_right {a b : A} (H : a ≤ b) (c : A) : a - c ≤ b - c := add_le_add_right H (-c)
 
   theorem sub_le_sub {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a - d ≤ b - c :=
-  add_le_add Hab (neg_le_neg_of_le Hcd)
+  add_le_add Hab (neg_le_neg Hcd)
 
   theorem sub_lt_sub_left {a b : A} (H : a < b) (c : A) : c - b < c - a :=
-  add_lt_add_left (neg_lt_neg_of_lt H) c
+  add_lt_add_left (neg_lt_neg H) c
 
   theorem sub_lt_sub_right {a b : A} (H : a < b) (c : A) : a - c < b - c := add_lt_add_right H (-c)
 
-  theorem sub_lt_sub_of_lt_of_lt {a b c d : A} (Hab : a < b) (Hcd : c < d) : a - d < b - c :=
-  add_lt_add_of_lt_of_lt Hab (neg_lt_neg_of_lt Hcd)
+  theorem sub_lt_sub {a b c d : A} (Hab : a < b) (Hcd : c < d) : a - d < b - c :=
+  add_lt_add Hab (neg_lt_neg Hcd)
 
   theorem sub_lt_sub_of_le_of_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a - d < b - c :=
-  add_lt_add_of_le_of_lt Hab (neg_lt_neg_of_lt Hcd)
+  add_lt_add_of_le_of_lt Hab (neg_lt_neg Hcd)
 
   theorem sub_lt_sub_of_lt_of_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a - d < b - c :=
-  add_lt_add_of_lt_of_le Hab (neg_le_neg_of_le Hcd)
-
+  add_lt_add_of_lt_of_le Hab (neg_le_neg Hcd)
 end
 
 -- TODO: additional facts if the ordering is a linear ordering (e.g. -a = a ↔ a = 0)
-
--- TODO: structures with abs
+-- TODO: abs and sign
 
 end algebra
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index be37dec55..eee162d5e 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -5,17 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: algebra.ordered_ring
 Authors: Jeremy Avigad
 
-Rather than multiply classes unnecessarily, we are aiming for the ones that are likely to be useful.
-We can always split them apart later if necessary. Here an "ordered_ring" is partial ordered ring (which
-is ordered with respect to both a weak order and an associated strict order). Our numeric structures will be
-instances of "linear_ordered_comm_ring".
-
-This development is modeled after Isabelle's library.
+Here an "ordered_ring" is partially ordered ring, which is ordered with respect to both a weak
+order and an associated strict order. Our numeric structures (int, rat, and real) will be instances
+of "linear_ordered_comm_ring". This development is modeled after Isabelle's library.
 -/
 
-import logic.eq data.unit data.sigma data.prod
-import algebra.function algebra.binary algebra.ordered_group algebra.ring
-
+import algebra.ordered_group algebra.ring
 open eq eq.ops
 
 namespace algebra
@@ -23,13 +18,12 @@ namespace algebra
 variable {A : Type}
 
 structure ordered_semiring [class] (A : Type) extends semiring A, ordered_cancel_comm_monoid A :=
-(mul_le_mul_left: ∀a b c, le a b → le zero c → le (mul c a) (mul c b))
-(mul_le_mul_right: ∀a b c, le a b → le zero c → le (mul a c) (mul b c))
-(mul_lt_mul_left: ∀a b c, lt a b → lt zero c → lt (mul c a) (mul c b))
-(mul_lt_mul_right: ∀a b c, lt a b → lt zero c → lt (mul a c) (mul b c))
+(mul_le_mul_of_nonneg_left: ∀a b c, le a b → le zero c → le (mul c a) (mul c b))
+(mul_le_mul_of_nonneg_right: ∀a b c, le a b → le zero c → le (mul a c) (mul b c))
+(mul_lt_mul_of_pos_left: ∀a b c, lt a b → lt zero c → lt (mul c a) (mul c b))
+(mul_lt_mul_of_pos_right: ∀a b c, lt a b → lt zero c → lt (mul a c) (mul b c))
 
 section
-
   variable [s : ordered_semiring A]
   variables (a b c d e : A)
   include s
@@ -43,10 +37,10 @@ section
   has_zero.mk (@ordered_semiring.zero A s)
 
   theorem mul_le_mul_of_nonneg_left {a b c : A} (Hab : a ≤ b) (Hc : 0 ≤ c) :
-    c * a ≤ c * b := !ordered_semiring.mul_le_mul_left Hab Hc
+    c * a ≤ c * b := !ordered_semiring.mul_le_mul_of_nonneg_left Hab Hc
 
   theorem mul_le_mul_of_nonneg_right {a b c : A} (Hab : a ≤ b) (Hc : 0 ≤ c) :
-    a * c ≤ b * c := !ordered_semiring.mul_le_mul_right Hab Hc
+    a * c ≤ b * c := !ordered_semiring.mul_le_mul_of_nonneg_right Hab Hc
 
   -- TODO: there are four variations, depending on which variables we assume to be nonneg
   theorem mul_le_mul {a b c d : A} (Hac : a ≤ c) (Hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) :
@@ -55,7 +49,7 @@ section
     a * b ≤ c * b : mul_le_mul_of_nonneg_right Hac nn_b
       ... ≤ c * d : mul_le_mul_of_nonneg_left Hbd nn_c
 
-  theorem mul_nonneg_of_nonneg_of_nonneg {a b : A} (Ha : a ≥ 0) (Hb : b ≥ 0) : a * b ≥ 0 :=
+  theorem mul_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 ▸ H
 
@@ -68,10 +62,10 @@ section
   !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
+    c * a < c * b := !ordered_semiring.mul_lt_mul_of_pos_left Hab Hc
 
   theorem mul_lt_mul_of_pos_right {a b c : A} (Hab : a < b) (Hc : 0 < c) :
-    a * c < b * c := !ordered_semiring.mul_lt_mul_right Hab Hc
+    a * c < b * c := !ordered_semiring.mul_lt_mul_of_pos_right Hab Hc
 
   -- TODO: once again, there are variations
   theorem mul_lt_mul {a b c d : A} (Hac : a < c) (Hbd : b ≤ d) (pos_b : 0 < b) (nn_c : 0 ≤ c) :
@@ -80,7 +74,7 @@ section
     a * b < c * b : mul_lt_mul_of_pos_right Hac pos_b
       ... ≤ c * d : mul_le_mul_of_nonneg_left Hbd nn_c
 
-  theorem mul_pos_of_pos_of_pos {a b : A} (Ha : a > 0) (Hb : b > 0) : a * b > 0 :=
+  theorem mul_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 ▸ H
 
@@ -91,16 +85,14 @@ section
   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 ▸ H
-
 end
 
 structure linear_ordered_semiring [class] (A : Type)
     extends ordered_semiring A, linear_strong_order_pair A
 
 section
-
   variable [s : linear_ordered_semiring A]
-  variables (a b c : A)
+  variables {a b c : A}
   include s
 
   -- TODO: remove after we short-circuit class-graph
@@ -111,25 +103,25 @@ section
   definition linear_ordered_semiring.to_zero [instance] [priority 100000] : has_zero A :=
   has_zero.mk (@linear_ordered_semiring.zero A s)
 
-  theorem lt_of_mul_lt_mul_left {a b c : A} (H : c * a < c * b) (Hc : c ≥ 0) : a < b :=
+  theorem lt_of_mul_lt_mul_left (H : c * a < c * b) (Hc : c ≥ 0) : a < b :=
   lt_of_not_le
     (assume H1 : b ≤ a,
       have H2 : c * b ≤ c * a, from mul_le_mul_of_nonneg_left H1 Hc,
       not_lt_of_le H2 H)
 
-  theorem lt_of_mul_lt_mul_right {a b c : A} (H : a * c < b * c) (Hc : c ≥ 0) : a < b :=
+  theorem lt_of_mul_lt_mul_right (H : a * c < b * c) (Hc : c ≥ 0) : a < b :=
   lt_of_not_le
     (assume H1 : b ≤ a,
       have H2 : b * c ≤ a * c, from mul_le_mul_of_nonneg_right H1 Hc,
       not_lt_of_le H2 H)
 
-  theorem le_of_mul_le_mul_left {a b c : A} (H : c * a ≤ c * b) (Hc : c > 0) : a ≤ b :=
+  theorem le_of_mul_le_mul_left (H : c * a ≤ c * b) (Hc : c > 0) : a ≤ b :=
   le_of_not_lt
     (assume H1 : b < a,
       have H2 : c * b < c * a, from mul_lt_mul_of_pos_left H1 Hc,
       not_le_of_lt H2 H)
 
-  theorem le_of_mul_le_mul_right {a b c : A} (H : a * c ≤ b * c) (Hc : c > 0) : a ≤ b :=
+  theorem le_of_mul_le_mul_right (H : a * c ≤ b * c) (Hc : c > 0) : a ≤ b :=
   le_of_not_lt
     (assume H1 : b < a,
       have H2 : b * c < a * c, from mul_lt_mul_of_pos_right H1 Hc,
@@ -146,21 +138,21 @@ section
     (assume H2 : a ≤ 0,
       have H3 : a * b ≤ 0, from mul_nonpos_of_nonpos_of_nonneg H2 H1,
       not_lt_of_le H3 H)
-
 end
 
 structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A :=
-(mul_nonneg_of_nonneg_of_nonneg : ∀a b, le zero a → le zero b → le zero (mul a b))
-(mul_pos_of_pos_of_pos : ∀a b, lt zero a → lt zero b → lt zero (mul a b))
+(mul_nonneg : ∀a b, le zero a → le zero b → le zero (mul a b))
+(mul_pos : ∀a b, lt zero a → lt zero b → lt zero (mul a b))
 
-definition ordered_ring.to_ordered_semiring [instance] [s : ordered_ring A] : ordered_semiring A :=
+definition ordered_ring.to_ordered_semiring [instance] [coercion] [s : ordered_ring A] :
+  ordered_semiring A :=
 ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
   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 _)
-  ordered_ring.le ordered_ring.le_refl ordered_ring.le_trans ordered_ring.le_antisym
+  ordered_ring.le ordered_ring.le_refl ordered_ring.le_trans ordered_ring.le_antisymm
   ordered_ring.lt ordered_ring.lt_iff_le_ne ordered_ring.add_le_add_left
   (@le_of_add_le_add_left A _)
   (take a b c,
@@ -169,7 +161,7 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
     show c * a ≤ c * b,
     proof
       have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab,
-      have H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg_of_nonneg_of_nonneg _ _ Hc H1,
+      have H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg _ _ Hc H1,
       iff.mp !sub_nonneg_iff_le (!mul_sub_left_distrib ▸ H2)
     qed)
   (take a b c,
@@ -178,7 +170,7 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
     show a * c ≤ b * c,
     proof
       have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab,
-      have H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg_of_nonneg_of_nonneg _ _ H1 Hc,
+      have H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg _ _ H1 Hc,
       iff.mp !sub_nonneg_iff_le (!mul_sub_right_distrib ▸ H2)
     qed)
   (take a b c,
@@ -187,7 +179,7 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
     show c * a < c * b,
     proof
       have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
-      have H2 : 0 < c * (b - a), from ordered_ring.mul_pos_of_pos_of_pos _ _ Hc H1,
+      have H2 : 0 < c * (b - a), from ordered_ring.mul_pos _ _ Hc H1,
       iff.mp !sub_pos_iff_lt (!mul_sub_left_distrib ▸ H2)
     qed)
   (take a b c,
@@ -196,14 +188,13 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
     show a * c < b * c,
     proof
       have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
-      have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos_of_pos_of_pos _ _ H1 Hc,
+      have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc,
       iff.mp !sub_pos_iff_lt (!mul_sub_right_distrib ▸ H2)
     qed)
 
 section
-
   variable [s : ordered_ring A]
-  variables (a b c : A)
+  variables {a b c : A}
   include s
 
   -- TODO: remove after we short-circuit class-graph
@@ -214,65 +205,107 @@ section
   definition ordered_ring.to_zero [instance] [priority 100000] : has_zero A :=
   has_zero.mk (@ordered_ring.zero A s)
 
-  theorem mul_le_mul_of_nonpos_left {a b c : A} (H : b ≤ a) (Hc : c ≤ 0) : c * a ≤ c * b :=
+  theorem mul_le_mul_of_nonpos_left (H : b ≤ a) (Hc : c ≤ 0) : c * a ≤ c * b :=
   have Hc' : -c ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos Hc,
   have H1 : -c * b ≤ -c * a, from mul_le_mul_of_nonneg_left H Hc',
   have H2 : -(c * b) ≤ -(c * a), from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_mul_eq_neg_mul⁻¹ ▸ H1,
   iff.mp !neg_le_neg_iff_le H2
 
-  theorem mul_le_mul_of_nonpos_right {a b c : A} (H : b ≤ a) (Hc : c ≤ 0) : a * c ≤ b * c :=
+  theorem mul_le_mul_of_nonpos_right (H : b ≤ a) (Hc : c ≤ 0) : a * c ≤ b * c :=
   have Hc' : -c ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos Hc,
   have H1 : b * -c ≤ a * -c, from mul_le_mul_of_nonneg_right H Hc',
   have H2 : -(b * c) ≤ -(a * c), from !neg_mul_eq_mul_neg⁻¹ ▸ !neg_mul_eq_mul_neg⁻¹ ▸ H1,
   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 :=
+  theorem mul_nonneg_of_nonpos_of_nonpos (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a * b :=
   !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 :=
+  theorem mul_lt_mul_of_neg_left (H : b < a) (Hc : c < 0) : c * a < c * b :=
   have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc,
   have H1 : -c * b < -c * a, from mul_lt_mul_of_pos_left H Hc',
   have H2 : -(c * b) < -(c * a), from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_mul_eq_neg_mul⁻¹ ▸ H1,
   iff.mp !neg_lt_neg_iff_lt H2
 
-  theorem mul_lt_mul_of_neg_right {a b c : A} (H : b < a) (Hc : c < 0) : a * c < b * c :=
+  theorem mul_lt_mul_of_neg_right (H : b < a) (Hc : c < 0) : a * c < b * c :=
   have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc,
   have H1 : b * -c < a * -c, from mul_lt_mul_of_pos_right H Hc',
   have H2 : -(b * c) < -(a * c), from !neg_mul_eq_mul_neg⁻¹ ▸ !neg_mul_eq_mul_neg⁻¹ ▸ H1,
   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 :=
+  theorem mul_pos_of_neg_of_neg (Ha : a < 0) (Hb : b < 0) : 0 < a * b :=
   !zero_mul ▸ mul_lt_mul_of_neg_right Ha Hb
-
 end
 
--- TODO: we can eliminate mul_pos_of_pos, but now it is not worth the effort to redeclare the class instance
+-- TODO: we can eliminate mul_pos_of_pos, but now it is not worth the effort to redeclare the
+-- class instance
 structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_strong_order_pair A
 
--- TODO: after we break out definition of divides, show that this is an instance of integral domain,
---   i.e no zero divisors
+-- print fields linear_ordered_semiring
+
+definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion]
+    [s : linear_ordered_ring A] :
+  linear_ordered_semiring A :=
+linear_ordered_semiring.mk linear_ordered_ring.add linear_ordered_ring.add_assoc
+  (@linear_ordered_ring.zero _ _) linear_ordered_ring.zero_add linear_ordered_ring.add_zero
+  linear_ordered_ring.add_comm linear_ordered_ring.mul linear_ordered_ring.mul_assoc
+  (@linear_ordered_ring.one _ _) linear_ordered_ring.one_mul linear_ordered_ring.mul_one
+  linear_ordered_ring.left_distrib linear_ordered_ring.right_distrib
+  zero_mul mul_zero !ordered_ring.zero_ne_one
+  (@add.left_cancel A _) (@add.right_cancel A _)
+  linear_ordered_ring.le linear_ordered_ring.le_refl linear_ordered_ring.le_trans
+  linear_ordered_ring.le_antisymm
+  linear_ordered_ring.lt linear_ordered_ring.lt_iff_le_ne linear_ordered_ring.add_le_add_left
+  (@le_of_add_le_add_left A _)
+  (@mul_le_mul_of_nonneg_left A _) (@mul_le_mul_of_nonneg_right A _)
+  (@mul_lt_mul_of_pos_left A _) (@mul_lt_mul_of_pos_right A _)
+  linear_ordered_ring.le_iff_lt_or_eq linear_ordered_ring.le_total
+
+structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A
+
+-- Linearity implies no zero divisors. Doesn't need commutativity.
+definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion]
+    [s: linear_ordered_comm_ring A] :
+  integral_domain A :=
+integral_domain.mk linear_ordered_comm_ring.add linear_ordered_comm_ring.add_assoc
+  (@linear_ordered_comm_ring.zero _ _)
+  linear_ordered_comm_ring.zero_add linear_ordered_comm_ring.add_zero
+  linear_ordered_comm_ring.neg linear_ordered_comm_ring.add_left_inv
+  linear_ordered_comm_ring.add_comm
+  linear_ordered_comm_ring.mul linear_ordered_comm_ring.mul_assoc
+  (@linear_ordered_comm_ring.one _ _)
+  linear_ordered_comm_ring.one_mul linear_ordered_comm_ring.mul_one
+  linear_ordered_comm_ring.left_distrib linear_ordered_comm_ring.right_distrib
+  (@linear_ordered_comm_ring.zero_ne_one _ _)
+  linear_ordered_comm_ring.mul_comm
+  (take a b,
+    assume H : a * b = 0,
+    show a = 0 ∨ b = 0, from
+      lt.by_cases
+        (assume Ha : 0 < a,
+          lt.by_cases
+            (assume Hb : 0 < b, absurd (H ▸ mul_pos Ha Hb) (lt.irrefl 0))
+            (assume Hb : 0 = b, or.inr (Hb⁻¹))
+            (assume Hb : 0 > b, absurd (H ▸ mul_neg_of_pos_of_neg Ha Hb) (lt.irrefl 0)))
+        (assume Ha : 0 = a, or.inl (Ha⁻¹))
+        (assume Ha : 0 > a,
+          lt.by_cases
+            (assume Hb : 0 < b, absurd (H ▸ mul_neg_of_neg_of_pos Ha Hb) (lt.irrefl 0))
+            (assume Hb : 0 = b, or.inr (Hb⁻¹))
+            (assume Hb : 0 > b, absurd (H ▸ mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0))))
 
 section
-
   variable [s : linear_ordered_ring A]
   variables (a b c : A)
   include s
 
   theorem mul_self_nonneg : a * a ≥ 0 :=
   or.elim (le.total 0 a)
-    (assume H : a ≥ 0, mul_nonneg_of_nonneg_of_nonneg H H)
+    (assume H : a ≥ 0, mul_nonneg H H)
     (assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H)
 
   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_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 :=
   has_mul.mk (@linear_ordered_ring.mul A s)
@@ -281,49 +314,25 @@ section
   definition linear_ordered_ring.to_zero [instance] [priority 100000] : has_zero A :=
   has_zero.mk (@linear_ordered_ring.zero A s)
 
-  /- TODO: a good example of a performance bottleneck.
-
-  Without any of the "proof ... qed" pairs, it exceeds the unifier maximum number of steps.
-
-  It works with at least one "proof ... qed", but takes about two seconds on my laptop. I do not
-  know where the bottleneck is.
-
-  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 ▸ 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) :
+  theorem pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) :
     (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
-  lt_or_eq_or_lt_cases
+  lt.by_cases
     (assume Ha : 0 < a,
-      lt_or_eq_or_lt_cases
+      lt.by_cases
         (assume Hb : 0 < b, or.inl (and.intro Ha Hb))
         (assume Hb : 0 = b,
           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))))
+          absurd Hab (lt.asymm (mul_neg_of_pos_of_neg Ha Hb))))
     (assume Ha : 0 = a,
       absurd (!zero_mul ▸ Ha⁻¹ ▸ Hab) (lt.irrefl 0))
     (assume Ha : a < 0,
-      lt_or_eq_or_lt_cases
+      lt.by_cases
         (assume Hb : 0 < b,
-          absurd Hab (not_lt_of_lt (mul_neg_of_neg_of_pos Ha Hb)))
+          absurd Hab (lt.asymm (mul_neg_of_neg_of_pos Ha Hb)))
         (assume Hb : 0 = b,
           absurd (!mul_zero ▸ Hb⁻¹ ▸ Hab) (lt.irrefl 0))
         (assume Hb : b < 0, or.inr (and.intro Ha Hb)))
-
-  set_option pp.coercions true
-  set_option pp.implicit true
-  set_option pp.notation false
-  -- print definition pos_and_pos_or_neg_and_neg_of_mul_pos
-
-  -- TODO: use previous and integral domain
-  theorem noneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg (Hab : a * b ≥ 0) :
-    (a ≥ 0 ∧ b ≥ 0) ∨ (a ≤ 0 ∧ b ≤ 0) :=
-  sorry
-
 end
 
 /-
@@ -337,6 +346,4 @@ end
   Multiplication and one, starting with mult_right_le_one_le.
 -/
 
-structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A
-
 end algebra
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index dcb8b882a..f611932cd 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -11,7 +11,6 @@ The development is modeled after Isabelle's library.
 
 import logic.eq logic.connectives data.unit data.sigma data.prod
 import algebra.function algebra.binary algebra.group
-
 open eq eq.ops
 
 namespace algebra
@@ -48,7 +47,6 @@ structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distr
     mul_zero_class A, zero_ne_one_class A
 
 section semiring
-
   variables [s : semiring A] (a b c : A)
   include s
 
@@ -61,17 +59,15 @@ section semiring
   assume H1 : b = 0,
   have H2 : a * b = 0, from H1⁻¹ ▸ mul_zero a,
   H H2
-
 end semiring
 
 /- comm semiring -/
 
 structure comm_semiring [class] (A : Type) extends semiring A, comm_semigroup A
-
--- TODO: we could also define a cancelative comm_semiring, i.e. satisfying c ≠ 0 → c * a = c * b → a = b.
+-- TODO: we could also define a cancelative comm_semiring, i.e. satisfying
+-- c ≠ 0 → c * a = c * b → a = b.
 
 section comm_semiring
-
   variables [s : comm_semiring A] (a b c : A)
   include s
 
@@ -81,6 +77,9 @@ section comm_semiring
   theorem dvd.intro {a b c : A} (H : a * b = c) : a | c :=
   exists.intro _ H
 
+  theorem dvd.intro_right {a b c : A} (H : a * b = c) : b | c :=
+  dvd.intro (!mul.comm ▸ H)
+
   theorem dvd.ex {a b : A} (H : a | b) : ∃c, a * c = b := H
 
   theorem dvd.elim {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, a * c = b → P) : P :=
@@ -147,15 +146,13 @@ section comm_semiring
       dvd.elim Hac
         (take e, assume Haec : a * e = c,
           dvd.intro (show a * (d + e) = b + c, from Hadb ▸ Haec ▸ left_distrib a d e)))
-
 end comm_semiring
 
-
 /- ring -/
 
 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 :=
+definition ring.to_semiring [instance] [coercion] [s : ring A] : semiring A :=
 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
@@ -177,7 +174,6 @@ semiring.mk ring.add ring.add_assoc !ring.zero ring.zero_add
   !ring.zero_ne_one
 
 section
-
   variables [s : ring A] (a b c d e : A)
   include s
 
@@ -225,12 +221,11 @@ section
       ... ↔ a * e + c - b * e = d : iff.symm !sub_eq_iff_eq_add
       ... ↔ a * e - b * e + c = d : !sub_add_eq_add_sub ▸ !iff.refl
       ... ↔ (a - b) * e + c = d : !mul_sub_right_distrib ▸ !iff.refl
-
 end
 
 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 :=
+definition comm_ring.to_comm_semiring [instance] [coercion] [s : comm_ring A] : comm_semiring A :=
 comm_semiring.mk comm_ring.add comm_ring.add_assoc (@comm_ring.zero A s)
   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
@@ -238,7 +233,6 @@ comm_semiring.mk comm_ring.add comm_ring.add_assoc (@comm_ring.zero A s)
   comm_ring.mul_comm
 
 section
-
   variables [s : comm_ring A] (a b c d e : A)
   include s
 
@@ -248,13 +242,6 @@ section
   theorem mul_self_sub_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
   mul_one 1 ▸ mul_self_sub_mul_self_eq a 1
 
-end
-
-section
-
-  variables [s : comm_ring A] (a b c d e : A)
-  include s
-
   theorem dvd_neg_iff_dvd : a | -b ↔ a | b :=
   iff.intro
     (assume H : a | -b,
@@ -292,14 +279,10 @@ section
 
   theorem dvd_sub (H₁ : a | b) (H₂ : a | c) : a | (b - c) :=
   dvd_add H₁ (iff.elim_right !dvd_neg_iff_dvd H₂)
-
 end
 
-
 /- integral domains -/
 
--- TODO: some properties here may extend to cancellative semirings. It is worth the effort?
-
 structure no_zero_divisors [class] (A : Type) extends has_mul A, has_zero A :=
 (eq_zero_or_eq_zero_of_mul_eq_zero : ∀a b, mul a b = zero → a = zero ∨ b = zero)
 
@@ -353,7 +336,6 @@ section
       have H1 : b * d * a = c * a, from eq.trans !mul.right_comm H,
       have H2 : b * d = c, from mul.cancel_right Ha H1,
       dvd.intro H2)
-
 end
 
 end algebra
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index a132d11ac..d359d6655 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -6,15 +6,15 @@ Module: int.basic
 Authors: Floris van Doorn, Jeremy Avigad
 
 The integers, with addition, multiplication, and subtraction. The representation of the integers is
-chosen to compute efficiently; see the examples in the comments at the end of this file.
+chosen to compute efficiently.
 
 To faciliate proving things about these operations, we show that the integers are a quotient of
-ℕ × ℕ with the usual equivalence relation ≡, and functions
+ℕ × ℕ with the usual equivalence relation, ≡, and functions
 
   abstr : ℕ × ℕ → ℤ
   repr : ℤ → ℕ × ℕ
 
-satisfying
+satisfying:
 
   abstr_repr (a : ℤ) : abstr (repr a) = a
   repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p
@@ -25,12 +25,12 @@ following:
 
   repr_add (a b : ℤ) : repr (a + b) = padd (repr a) (repr b)
   padd_congr (p p' q q' : ℕ × ℕ) (H1 : p ≡ p') (H2 : q ≡ q') : padd p q ≡ p' q'
+
 -/
 
 import data.nat.basic data.nat.order data.nat.sub data.prod
 import algebra.relation algebra.binary algebra.ordered_ring
 import tools.fake_simplifier
-
 open eq.ops
 open prod relation nat
 open decidable binary fake_simplifier
@@ -54,8 +54,8 @@ nat.cases_on m 0 (take m', neg_succ_of_nat m')
 
 definition sub_nat_nat (m n : ℕ) : ℤ :=
 nat.cases_on (n - m)
-  (of_nat (m - n))     -- m ≥ n
-  (take k, neg_succ_of_nat k)   -- m < n, and n - m = succ k
+  (of_nat (m - n))                                     -- m ≥ n
+  (take k, neg_succ_of_nat k)                          -- m < n, and n - m = succ k
 
 definition neg (a : ℤ) : ℤ :=
   cases_on a
@@ -144,11 +144,7 @@ cases_on a
   (take m, assume H : nat_abs (of_nat m) = 0, congr_arg of_nat H)
   (take m', assume H : nat_abs (neg_succ_of_nat m') = 0, absurd H (succ_ne_zero _))
 
-
-/-
-Show int is a quotient of ordered pairs of natural numbers, with the usual
-equivalence relation.
--/
+/- int is a quotient of ordered pairs of natural numbers -/
 
 definition equiv (p q : ℕ × ℕ) : Prop :=  pr1 p + pr2 q = pr2 p + pr1 q
 
@@ -319,7 +315,7 @@ or.elim (cases_of_nat_succ a)
   (assume H, obtain (n : ℕ) (H3 : a = -(succ n)), from H, H3⁻¹ ▸ H2 n)
 
 /-
-Show int is a ring.
+   int is a ring
 -/
 
 /- addition -/
@@ -434,7 +430,7 @@ have H : repr (-a + a) ≡ repr 0, from
       ... ≡ repr 0 : padd_pneg,
 eq_of_repr_equiv_repr H
 
-/- nat -/
+/- nat abs -/
 
 definition pabs (p : ℕ × ℕ) : ℕ := dist (pr1 p) (pr2 p)
 
@@ -595,24 +591,27 @@ 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 eq_zero_or_eq_zero_of_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)
 
-definition integral_domain : algebra.integral_domain int :=
+protected definition integral_domain : algebra.integral_domain int :=
 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
 
-/-
-Instantiate ring theorems to int
--/
+--namespace algebra
+--  open algebra    -- TODO: why do we have to do this?
+--  instance [persistent] int.integral_domain
+--end algebra
 
--- TODO: make this "section" when scoping bug is fixed
-context port_algebra
+/- instantiate ring theorems to int -/
+
+section port_algebra
   open algebra
-  instance integral_domain
+  instance int.integral_domain  -- TODO: why didn't the setting above persist?
 
   theorem mul.left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
   theorem mul.right_comm : ∀a b c : ℤ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
@@ -687,6 +686,7 @@ context port_algebra
   definition dvd (a b : ℤ) : Prop := algebra.dvd a b
   infix `|` := dvd
   theorem dvd.intro : ∀{a b c : ℤ} (H : a * b = c), a | c := @algebra.dvd.intro _ _
+  theorem dvd.intro_right : ∀{a b c : ℤ} (H : a * b = c), b | c := @algebra.dvd.intro_right _ _
   theorem dvd.ex : ∀{a b : ℤ} (H : a | b), ∃c, a * c = b := @algebra.dvd.ex _ _
   theorem dvd.elim : ∀{P : Prop} {a b : ℤ} (H₁ : a | b) (H₂ : ∀c, a * c = b → P), P :=
     @algebra.dvd.elim _ _
@@ -741,54 +741,6 @@ context port_algebra
     @algebra.dvd_of_mul_dvd_mul_left _ _
   theorem dvd_of_mul_dvd_mul_right : ∀{a b c : ℤ}, a ≠ 0 → b * a | c * a → b | c :=
     @algebra.dvd_of_mul_dvd_mul_right _ _
-
 end port_algebra
 
--- TODO: declare appropriate rewrite rules
--- 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
----- add_rewrite sub_sub_assoc sub_add_assoc add_sub_assoc
----- add_rewrite add_neg_right add_neg_left
----- add_rewrite sub_self
-
 end int
-
-
-/- tests -/
-
-/- open int
-
-eval -100
-eval -(-100)
-
-eval #int (5 + 7)
-eval -5 + 7
-eval 5 + -7
-eval -5 + -7
-
-eval #int 155 + 277
-eval -155 + 277
-eval 155 + -277
-eval -155 + -277
-
-eval #int 155 - 277
-eval #int 277 - 155
-
-eval #int 2 * 3
-eval -2 * 3
-eval 2 * -3
-eval -2 * -3
-
-eval 22 * 33
-eval -22 * 33
-eval 22 * -33
-eval -22 * -33
-
-eval #int 22 ≤ 33
-eval #int 33 ≤ 22
-
-example : #int 22 ≤ 33 := true.intro
-example : #int -5 < 7 := true.intro
--/
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 2efa3a06d..24007321f 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.int.order
 Authors: Floris van Doorn, Jeremy Avigad
 
-The order relation on the integers, and the sign function.
+The order relation on the integers. We show that int is an instance of linear_comm_ordered_ring
+and transfer the results.
 -/
 
-import .basic
+import .basic algebra.ordered_ring
 
 open nat
 open decidable
@@ -17,7 +18,7 @@ open int eq.ops
 
 namespace int
 
-definition nonneg (a : ℤ) : Prop := cases_on a (take n, true) (take n, false)
+private definition nonneg (a : ℤ) : Prop := cases_on a (take n, true) (take n, false)
 definition le (a b : ℤ) : Prop := nonneg (sub b a)
 definition lt (a b : ℤ) : Prop := le (add a 1) b
 
@@ -26,52 +27,88 @@ infix <= := int.le
 infix ≤  := int.le
 infix <  := int.lt
 
-definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := cases_on a _ _
+private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := cases_on a _ _
 definition decidable_le [instance] (a b : ℤ) : decidable (a ≤ b) := decidable_nonneg _
 definition decidable_lt [instance] (a b : ℤ) : decidable (a < b) := decidable_nonneg _
 
-theorem nonneg_elim {a : ℤ} : nonneg a → ∃n : ℕ, a = n :=
+private theorem nonneg.elim {a : ℤ} : nonneg a → ∃n : ℕ, a = n :=
 cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H)
 
-theorem le_intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
+private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) :=
+cases_on a (take n, or.inl trivial) (take n, or.inr trivial)
+
+theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
 have H1 : b - a = n, from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹,
 have H2 : nonneg n, from true.intro,
 show nonneg (b - a), from H1⁻¹ ▸ H2
 
-theorem le_elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
-obtain (n : ℕ) (H1 : b - a = n), from nonneg_elim H,
+theorem le.elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
+obtain (n : ℕ) (H1 : b - a = n), from nonneg.elim H,
 exists.intro n (!add.comm ▸ iff.mp' !add_eq_iff_eq_add_neg (H1⁻¹))
 
--- ### partial order
+theorem le.total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
+or.elim (nonneg_or_nonneg_neg (b - a))
+  (assume H, or.inl H)
+  (assume H : nonneg (-(b - a)),
+    have H0 : -(b - a) = a - b, from neg_sub_eq b a,
+    have H1 : nonneg (a - b), from H0 ▸ H,    -- too bad: can't do it in one step
+    or.inr H1)
 
-theorem le_refl (a : ℤ) : a ≤ a :=
-le_intro (add_zero a)
-
-theorem le_of_nat (n m : ℕ) : (of_nat n ≤ of_nat m) ↔ (n ≤ m) :=
+theorem of_nat_le_of_nat (n m : ℕ) : of_nat n ≤ of_nat m ↔ n ≤ m :=
 iff.intro
   (assume H : of_nat n ≤ of_nat m,
-    obtain (k : ℕ) (Hk : of_nat n + of_nat k = of_nat m), from le_elim H,
+    obtain (k : ℕ) (Hk : of_nat n + of_nat k = of_nat m), from le.elim H,
     have H2 : n + k = m, from of_nat_inj ((add_of_nat n k)⁻¹ ⬝ Hk),
     nat.le_intro H2)
   (assume H : n ≤ m,
     obtain (k : ℕ) (Hk : n + k = m), from nat.le_elim H,
     have H2 : of_nat n + of_nat k = of_nat m, from Hk ▸ add_of_nat n k,
-    le_intro H2)
+    le.intro H2)
 
-theorem le_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
-obtain (n : ℕ) (Hn : a + n = b), from le_elim H1,
-obtain (m : ℕ) (Hm : b + m = c), from le_elim H2,
+theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n :=
+le.intro (show a + 1 + n = a + succ n, from
+  calc
+    a + 1 + n = a + (1 + n) : add.assoc
+      ... = a + (n + 1)     : add.comm
+      ... = a + succ n      : rfl)
+
+theorem lt.intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b :=
+H ▸ lt_add_succ a n
+
+theorem lt.elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b :=
+obtain (n : ℕ) (Hn : a + 1 + n = b), from le.elim H,
+have H2 : a + succ n = b, from
+  calc
+    a + succ n = a + 1 + n : by simp
+      ... = b : Hn,
+exists.intro n H2
+
+theorem of_nat_lt_of_nat (n m : ℕ) : of_nat n < of_nat m ↔ n < m :=
+calc
+  of_nat n < of_nat m ↔ of_nat n + 1 ≤ of_nat m : iff.refl
+    ... ↔ of_nat (succ n) ≤ of_nat m            : of_nat_succ n ▸ !iff.refl
+    ... ↔ succ n ≤ m                            : of_nat_le_of_nat
+    ... ↔ n < m                                 : iff.symm (lt_iff_succ_le _ _)
+
+/- show that the integers form an ordered additive group -/
+
+theorem le.refl (a : ℤ) : a ≤ a :=
+le.intro (add_zero a)
+
+theorem le.trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
+obtain (n : ℕ) (Hn : a + n = b), from le.elim H1,
+obtain (m : ℕ) (Hm : b + m = c), from le.elim H2,
 have H3 : a + of_nat (n + m) = c, from
   calc
     a + of_nat (n + m) = a + (of_nat n + m) : {(add_of_nat n m)⁻¹}
       ... = a + n + m : (add.assoc a n m)⁻¹
       ... = b + m : {Hn}
       ... = c : Hm,
-le_intro H3
+le.intro H3
 
-theorem le_antisym {a b : ℤ} (H1 : a ≤ b) (H2 : b ≤ a) : a = b :=
-obtain (n : ℕ) (Hn : a + n = b), from le_elim H1,
-obtain (m : ℕ) (Hm : b + m = a), from le_elim H2,
+theorem le.antisymm {a b : ℤ} (H1 : a ≤ b) (H2 : b ≤ a) : a = b :=
+obtain (n : ℕ) (Hn : a + n = b), from le.elim H1,
+obtain (m : ℕ) (Hm : b + m = a), from le.elim H2,
 have H3 : a + of_nat (n + m) = a + 0, from
   calc
     a + of_nat (n + m) = a + (of_nat n + m) : {(add_of_nat n m)⁻¹}
@@ -88,27 +125,388 @@ show a = b, from
       ... = a + n : {H6⁻¹}
       ... = b : Hn
 
--- ### interaction with add
+theorem lt.irrefl (a : ℤ) : ¬ a < a :=
+(assume H : a < a,
+  obtain (n : ℕ) (Hn : a + succ n = a), from lt.elim H,
+  have H2 : a + succ n = a + 0, from
+    calc
+      a + succ n = a : Hn
+        ... = a + 0 : by simp,
+  have H3 : succ n = 0, from add.left_cancel H2,
+  have H4 : succ n = 0, from of_nat_inj H3,
+  absurd H4 !succ_ne_zero)
 
-theorem le_add_of_nat_right (a : ℤ) (n : ℕ) : a ≤ a + n :=
-le_intro (eq.refl (a + n))
+theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b :=
+(assume H2 : a = b, absurd (H2 ▸ H) (lt.irrefl b))
 
-theorem le_add_of_nat_left (a : ℤ) (n : ℕ) : a ≤ n + a :=
-le_intro (add.comm a n)
+theorem succ_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b := H
 
-theorem add_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b :=
-obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
+theorem lt_of_le_succ {a b : ℤ} (H : a + 1 ≤ b) : a < b := H
+
+theorem le_of_lt {a b : ℤ} (H : a < b) : a ≤ b :=
+obtain (n : ℕ) (Hn : a + succ n = b), from lt.elim H,
+le.intro Hn
+
+theorem lt_iff_le_and_ne (a b : ℤ) : a < b ↔ (a ≤ b ∧ a ≠ b) :=
+iff.intro
+  (assume H, and.intro (le_of_lt H) (ne_of_lt H))
+  (assume H,
+    have H1 : a ≤ b, from and.elim_left H,
+    have H2 : a ≠ b, from and.elim_right H,
+    obtain (n : ℕ) (Hn : a + n = b), from le.elim H1,
+    have H3 : n ≠ 0, from (assume H' : n = 0, H2 (!add_zero ▸ H' ▸ Hn)),
+    obtain (k : ℕ) (Hk : n = succ k), from nat.exists_eq_succ_of_ne_zero H3,
+    lt.intro (Hk ▸ Hn))
+
+theorem le_iff_lt_or_eq (a b : ℤ) : a ≤ b ↔ (a < b ∨ a = b) :=
+iff.intro
+  (assume H,
+    by_cases
+      (assume H1 : a = b, or.inr H1)
+      (assume H1 : a ≠ b,
+        obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
+        have H2 : n ≠ 0, from (assume H' : n = 0, H1 (!add_zero ▸ H' ▸ Hn)),
+        obtain (k : ℕ) (Hk : n = succ k), from nat.exists_eq_succ_of_ne_zero H2,
+        or.inl (lt.intro (Hk ▸ Hn))))
+  (assume H,
+    or.elim H
+      (assume H1, le_of_lt H1)
+      (assume H1, H1 ▸ !le.refl))
+
+theorem lt_succ (a : ℤ) : a < a + 1 :=
+le.refl (a + 1)
+
+theorem add_le_add_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b :=
+obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
 have H2 : c + a + n = c + b, from
   calc
     c + a + n = c + (a + n) : add.assoc c a n
       ... = c + b : {Hn},
-le_intro H2
+le.intro H2
+
+theorem mul_nonneg {a b : ℤ} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a * b :=
+obtain (n : ℕ) (Hn : 0 + n = a), from le.elim Ha,
+obtain (m : ℕ) (Hm : 0 + m = b), from le.elim Hb,
+le.intro
+  (eq.symm
+    (calc
+      a * b = (0 + n) * b : Hn
+        ... = n * b       : zero_add
+        ... = n * (0 + m) : Hm
+        ... = n * m       : zero_add
+        ... = 0 + n * m   : zero_add))
+
+theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b :=
+obtain (n : ℕ) (Hn : 0 + succ n = a), from lt.elim Ha,
+obtain (m : ℕ) (Hm : 0 + succ m = b), from lt.elim Hb,
+lt.intro
+  (eq.symm
+    (calc
+      a * b = (0 + succ n) * b                 : Hn
+        ... = succ n * b                       : zero_add
+        ... = succ n * (0 + succ m)            : Hm
+        ... = succ n * succ m                  : zero_add
+        ... = of_nat (succ n * succ m)         : mul_of_nat
+        ... = of_nat (succ n * m + succ n)     : nat.mul_succ
+        ... = of_nat (succ (succ n * m + n))   : nat.add_succ
+        ... = 0 + succ (succ n * m + n)        : zero_add))
+
+protected definition linear_ordered_comm_ring : algebra.linear_ordered_comm_ring int :=
+algebra.linear_ordered_comm_ring.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 le le.refl @le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left
+  @mul_nonneg @mul_pos le_iff_lt_or_eq le.total mul.comm
+
+/- instantiate ordered ring theorems to int -/
+
+namespace algebra
+  open algebra
+  instance [persistent] int.linear_ordered_comm_ring
+end algebra
+
+section port_algebra
+  open algebra
+  instance int.linear_ordered_comm_ring
+
+  definition ge (a b : ℤ) := algebra.has_le.ge a b
+  definition gt (a b : ℤ) := algebra.has_lt.gt a b
+  infix >= := int.ge
+  infix ≥  := int.ge
+  infix >  := int.gt
+  definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) := _
+  definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) := _
+
+  theorem le_of_eq_of_le : ∀{a b c : ℤ}, a = b → b ≤ c → a ≤ c := @algebra.le_of_eq_of_le _ _
+  theorem le_of_le_of_eq : ∀{a b c : ℤ}, a ≤ b → b = c → a ≤ c := @algebra.le_of_le_of_eq _ _
+  theorem lt_of_eq_of_lt : ∀{a b c : ℤ}, a = b → b < c → a < c := @algebra.lt_of_eq_of_lt _ _
+  theorem lt_of_lt_of_eq : ∀{a b c : ℤ}, a < b → b = c → a < c := @algebra.lt_of_lt_of_eq _ _
+  calc_trans int.le_of_eq_of_le
+  calc_trans int.le_of_le_of_eq
+  calc_trans int.lt_of_eq_of_lt
+  calc_trans int.lt_of_lt_of_eq
+
+  theorem lt.asymm : ∀{a b : ℤ}, a < b → ¬ b < a := @algebra.lt.asymm _ _
+  theorem lt_of_le_of_ne : ∀{a b : ℤ}, a ≤ b → a ≠ b → a < b := @algebra.lt_of_le_of_ne _ _
+  theorem lt_of_lt_of_le : ∀{a b c : ℤ}, a < b → b ≤ c → a < c := @algebra.lt_of_lt_of_le _ _
+  theorem lt_of_le_of_lt : ∀{a b c : ℤ}, a ≤ b → b < c → a < c := @algebra.lt_of_le_of_lt _ _
+  theorem not_le_of_lt : ∀{a b : ℤ}, a < b → ¬ b ≤ a := @algebra.not_le_of_lt _ _
+  theorem not_lt_of_le : ∀{a b : ℤ}, a ≤ b → ¬ b < a := @algebra.not_lt_of_le _ _
+
+  theorem lt_or_eq_of_le : ∀{a b : ℤ}, a ≤ b → a < b ∨ a = b := @algebra.lt_or_eq_of_le _ _
+  theorem lt.trichotomy : ∀a b : ℤ, a < b ∨ a = b ∨ b < a := algebra.lt.trichotomy
+  theorem lt.by_cases : ∀{a b : ℤ} {P : Prop}, (a < b → P) → (a = b → P) → (b < a → P) → P :=
+    @algebra.lt.by_cases _ _
+  definition le_of_not_lt : ∀{a b : ℤ}, ¬ a < b → b ≤ a := @algebra.le_of_not_lt _ _
+  definition lt_of_not_le : ∀{a b : ℤ}, ¬ a ≤ b → b < a := @algebra.lt_of_not_le _ _
+
+  theorem add_le_add_right : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, a + c ≤ b + c :=
+    @algebra.add_le_add_right _ _
+  theorem add_le_add : ∀{a b c d : ℤ}, a ≤ b → c ≤ d → a + c ≤ b + d := @algebra.add_le_add _ _
+  theorem add_lt_add_left : ∀{a b : ℤ}, a < b → ∀c : ℤ, c + a < c + b :=
+    @algebra.add_lt_add_left _ _
+  theorem add_lt_add_right : ∀{a b : ℤ}, a < b → ∀c : ℤ, a + c < b + c :=
+    @algebra.add_lt_add_right _ _
+  theorem le_add_of_nonneg_right : ∀{a b : ℤ}, b ≥ 0 → a ≤ a + b :=
+    @algebra.le_add_of_nonneg_right _ _
+  theorem le_add_of_nonneg_left : ∀{a b : ℤ}, b ≥ 0 → a ≤ b + a :=
+    @algebra.le_add_of_nonneg_left _ _
+  theorem add_lt_add : ∀{a b c d : ℤ}, a < b → c < d → a + c < b + d := @algebra.add_lt_add _ _
+  theorem add_lt_add_of_le_of_lt : ∀{a b c d : ℤ}, a ≤ b → c < d → a + c < b + d :=
+    @algebra.add_lt_add_of_le_of_lt _ _
+  theorem add_lt_add_of_lt_of_le : ∀{a b c d : ℤ}, a < b → c ≤ d → a + c < b + d :=
+    @algebra.add_lt_add_of_lt_of_le _ _
+  theorem lt_add_of_pos_right : ∀{a b : ℤ}, b > 0 → a < a + b := @algebra.lt_add_of_pos_right _ _
+  theorem lt_add_of_pos_left : ∀{a b : ℤ}, b > 0 → a < b + a := @algebra.lt_add_of_pos_left _ _
+  theorem le_of_add_le_add_left : ∀{a b c : ℤ}, a + b ≤ a + c → b ≤ c :=
+    @algebra.le_of_add_le_add_left _ _
+  theorem le_of_add_le_add_right : ∀{a b c : ℤ}, a + b ≤ c + b → a ≤ c :=
+    @algebra.le_of_add_le_add_right _ _
+  theorem lt_of_add_lt_add_left : ∀{a b c : ℤ}, a + b < a + c → b < c :=
+    @algebra.lt_of_add_lt_add_left _ _
+  theorem lt_of_add_lt_add_right : ∀{a b c : ℤ}, a + b < c + b → a < c :=
+    @algebra.lt_of_add_lt_add_right _ _
+  theorem add_le_add_left_iff : ∀a b c : ℤ, a + b ≤ a + c ↔ b ≤ c := algebra.add_le_add_left_iff
+  theorem add_le_add_right_iff : ∀a b c : ℤ, a + b ≤ c + b ↔ a ≤ c := algebra.add_le_add_right_iff
+  theorem add_lt_add_left_iff : ∀a b c : ℤ, a + b < a + c ↔ b < c := algebra.add_lt_add_left_iff
+  theorem add_lt_add_right_iff : ∀a b c : ℤ, a + b < c + b ↔ a < c := algebra.add_lt_add_right_iff
+  theorem add_nonneg : ∀{a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b := @algebra.add_nonneg _ _
+  theorem add_pos : ∀{a b : ℤ}, 0 < a → 0 < b → 0 < a + b := @algebra.add_pos _ _
+  theorem add_pos_of_pos_of_nonneg : ∀{a b : ℤ}, 0 < a → 0 ≤ b → 0 < a + b :=
+    @algebra.add_pos_of_pos_of_nonneg _ _
+  theorem add_pos_of_nonneg_of_pos : ∀{a b : ℤ}, 0 ≤ a → 0 < b → 0 < a + b :=
+    @algebra.add_pos_of_nonneg_of_pos _ _
+  theorem add_nonpos : ∀{a b : ℤ}, a ≤ 0 → b ≤ 0 → a + b ≤ 0 :=
+    @algebra.add_nonpos _ _
+  theorem add_neg : ∀{a b : ℤ}, a < 0 → b < 0 → a + b < 0 :=
+    @algebra.add_neg _ _
+  theorem add_neg_of_neg_of_nonpos : ∀{a b : ℤ}, a < 0 → b ≤ 0 → a + b < 0 :=
+    @algebra.add_neg_of_neg_of_nonpos _ _
+  theorem add_neg_of_nonpos_of_neg : ∀{a b : ℤ}, a ≤ 0 → b < 0 → a + b < 0 :=
+    @algebra.add_neg_of_nonpos_of_neg _ _
+  theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg : ∀{a b : ℤ},
+    0 ≤ a → 0 ≤ b → a + b = 0 ↔ a = 0 ∧ b = 0 :=
+    @algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _
+
+  theorem le_add_of_nonneg_of_le : ∀{a b c : ℤ}, 0 ≤ a → b ≤ c → b ≤ a + c :=
+    @algebra.le_add_of_nonneg_of_le _ _
+  theorem le_add_of_le_of_nonneg : ∀{a b c : ℤ}, b ≤ c → 0 ≤ a → b ≤ c + a :=
+    @algebra.le_add_of_le_of_nonneg _ _
+  theorem lt_add_of_pos_of_le : ∀{a b c : ℤ}, 0 < a → b ≤ c → b < a + c :=
+    @algebra.lt_add_of_pos_of_le _ _
+  theorem lt_add_of_le_of_pos : ∀{a b c : ℤ}, b ≤ c → 0 < a → b < c + a :=
+    @algebra.lt_add_of_le_of_pos _ _
+  theorem add_le_of_nonpos_of_le : ∀{a b c : ℤ}, a ≤ 0 → b ≤ c → a + b ≤ c :=
+    @algebra.add_le_of_nonpos_of_le _ _
+  theorem add_le_of_le_of_nonpos : ∀{a b c : ℤ}, b ≤ c → a ≤ 0 → b + a ≤ c :=
+    @algebra.add_le_of_le_of_nonpos _ _
+  theorem add_lt_of_neg_of_le : ∀{a b c : ℤ}, a < 0 → b ≤ c → a + b < c :=
+    @algebra.add_lt_of_neg_of_le _ _
+  theorem add_lt_of_le_of_neg : ∀{a b c : ℤ}, b ≤ c → a < 0 → b + a < c :=
+    @algebra.add_lt_of_le_of_neg _ _
+  theorem lt_add_of_nonneg_of_lt : ∀{a b c : ℤ}, 0 ≤ a → b < c → b < a + c :=
+    @algebra.lt_add_of_nonneg_of_lt _ _
+  theorem lt_add_of_lt_of_nonneg : ∀{a b c : ℤ}, b < c → 0 ≤ a → b < c + a :=
+    @algebra.lt_add_of_lt_of_nonneg _ _
+  theorem lt_add_of_pos_of_lt : ∀{a b c : ℤ}, 0 < a → b < c → b < a + c :=
+    @algebra.lt_add_of_pos_of_lt _ _
+  theorem lt_add_of_lt_of_pos : ∀{a b c : ℤ}, b < c → 0 < a → b < c + a :=
+    @algebra.lt_add_of_lt_of_pos _ _
+  theorem add_lt_of_nonpos_of_lt : ∀{a b c : ℤ}, a ≤ 0 → b < c → a + b < c :=
+    @algebra.add_lt_of_nonpos_of_lt _ _
+  theorem add_lt_of_lt_of_nonpos : ∀{a b c : ℤ}, b < c →  a ≤ 0 → b + a < c :=
+    @algebra.add_lt_of_lt_of_nonpos _ _
+  theorem add_lt_of_neg_of_lt : ∀{a b c : ℤ}, a < 0 → b < c → a + b < c :=
+    @algebra.add_lt_of_neg_of_lt _ _
+  theorem add_lt_of_lt_of_neg : ∀{a b c : ℤ}, b < c → a < 0 → b + a < c :=
+    @algebra.add_lt_of_lt_of_neg _ _
+
+  theorem neg_le_neg : ∀{a b : ℤ}, a ≤ b → -b ≤ -a := @algebra.neg_le_neg _ _
+  theorem neg_le_neg_iff_le : ∀a b : ℤ, -a ≤ -b ↔ b ≤ a := algebra.neg_le_neg_iff_le
+  theorem neg_nonpos_iff_nonneg : ∀a : ℤ, -a ≤ 0 ↔ 0 ≤ a := algebra.neg_nonpos_iff_nonneg
+  theorem neg_nonneg_iff_nonpos : ∀a : ℤ, 0 ≤ -a ↔ a ≤ 0 := algebra.neg_nonneg_iff_nonpos
+  theorem neg_lt_neg : ∀{a b : ℤ}, a < b → -b < -a := @algebra.neg_lt_neg _ _
+  theorem neg_lt_neg_iff_lt : ∀a b : ℤ, -a < -b ↔ b < a := algebra.neg_lt_neg_iff_lt
+  theorem neg_neg_iff_pos : ∀a : ℤ, -a < 0 ↔ 0 < a := algebra.neg_neg_iff_pos
+  theorem neg_pos_iff_neg : ∀a : ℤ, 0 < -a ↔ a < 0 := algebra.neg_pos_iff_neg
+  theorem le_neg_iff_le_neg : ∀a b : ℤ, a ≤ -b ↔ b ≤ -a := algebra.le_neg_iff_le_neg
+  theorem neg_le_iff_neg_le : ∀a b : ℤ, -a ≤ b ↔ -b ≤ a := algebra.neg_le_iff_neg_le
+  theorem lt_neg_iff_lt_neg : ∀a b : ℤ, a < -b ↔ b < -a := algebra.lt_neg_iff_lt_neg
+  theorem neg_lt_iff_neg_lt : ∀a b : ℤ, -a < b ↔ -b < a := algebra.neg_lt_iff_neg_lt
+  theorem sub_nonneg_iff_le : ∀a b : ℤ, 0 ≤ a - b ↔ b ≤ a := algebra.sub_nonneg_iff_le
+  theorem sub_nonpos_iff_le : ∀a b : ℤ, a - b ≤ 0 ↔ a ≤ b := algebra.sub_nonpos_iff_le
+  theorem sub_pos_iff_lt : ∀a b : ℤ, 0 < a - b ↔ b < a := algebra.sub_pos_iff_lt
+  theorem sub_neg_iff_lt : ∀a b : ℤ, a - b < 0 ↔ a < b := algebra.sub_neg_iff_lt
+  theorem add_le_iff_le_neg_add : ∀a b c : ℤ, a + b ≤ c ↔ b ≤ -a + c :=
+    algebra.add_le_iff_le_neg_add
+  theorem add_le_iff_le_sub_left : ∀a b c : ℤ, a + b ≤ c ↔ b ≤ c - a :=
+    algebra.add_le_iff_le_sub_left
+  theorem add_le_iff_le_sub_right : ∀a b c : ℤ, a + b ≤ c ↔ a ≤ c - b :=
+    algebra.add_le_iff_le_sub_right
+  theorem le_add_iff_neg_add_le : ∀a b c : ℤ, a ≤ b + c ↔ -b + a ≤ c :=
+    algebra.le_add_iff_neg_add_le
+  theorem le_add_iff_sub_left_le : ∀a b c : ℤ, a ≤ b + c ↔ a - b ≤ c :=
+    algebra.le_add_iff_sub_left_le
+  theorem le_add_iff_sub_right_le : ∀a b c : ℤ, a ≤ b + c ↔ a - c ≤ b :=
+    algebra.le_add_iff_sub_right_le
+  theorem add_lt_iff_lt_neg_add_left : ∀a b c : ℤ, a + b < c ↔ b < -a + c :=
+    algebra.add_lt_iff_lt_neg_add_left
+  theorem add_lt_iff_lt_neg_add_right : ∀a b c : ℤ, a + b < c ↔ a < -b + c :=
+    algebra.add_lt_iff_lt_neg_add_right
+  theorem add_lt_iff_lt_sub_left : ∀a b c : ℤ, a + b < c ↔ b < c - a :=
+    algebra.add_lt_iff_lt_sub_left
+  theorem add_lt_add_iff_lt_sub_right : ∀a b c : ℤ, a + b < c ↔ a < c - b :=
+    algebra.add_lt_add_iff_lt_sub_right
+  theorem lt_add_iff_neg_add_lt_left : ∀a b c : ℤ, a < b + c ↔ -b + a < c :=
+    algebra.lt_add_iff_neg_add_lt_left
+  theorem lt_add_iff_neg_add_lt_right : ∀a b c : ℤ, a < b + c ↔ -c + a < b :=
+    algebra.lt_add_iff_neg_add_lt_right
+  theorem lt_add_iff_sub_lt_left : ∀a b c : ℤ, a < b + c ↔ a - b < c :=
+    algebra.lt_add_iff_sub_lt_left
+  theorem lt_add_iff_sub_lt_right : ∀a b c : ℤ, a < b + c ↔ a - c < b :=
+    algebra.lt_add_iff_sub_lt_right
+  theorem le_iff_le_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a ≤ b ↔ c ≤ d :=
+    @algebra.le_iff_le_of_sub_eq_sub _ _
+  theorem lt_iff_lt_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a < b ↔ c < d :=
+    @algebra.lt_iff_lt_of_sub_eq_sub _ _
+  theorem sub_le_sub_left : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, c - b ≤ c - a :=
+    @algebra.sub_le_sub_left _ _
+  theorem sub_le_sub_right : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, a - c ≤ b - c :=
+    @algebra.sub_le_sub_right _ _
+  theorem sub_le_sub : ∀{a b c d : ℤ}, a ≤ b → c ≤ d → a - d ≤ b - c :=
+    @algebra.sub_le_sub _ _
+  theorem sub_lt_sub_left : ∀{a b : ℤ}, a < b → ∀c : ℤ, c - b < c - a :=
+    @algebra.sub_lt_sub_left _ _
+  theorem sub_lt_sub_right : ∀{a b : ℤ}, a < b → ∀c : ℤ, a - c < b - c :=
+    @algebra.sub_lt_sub_right _ _
+  theorem sub_lt_sub : ∀{a b c d : ℤ}, a < b → c < d → a - d < b - c :=
+    @algebra.sub_lt_sub _ _
+  theorem sub_lt_sub_of_le_of_lt : ∀{a b c d : ℤ}, a ≤ b → c < d → a - d < b - c :=
+    @algebra.sub_lt_sub_of_le_of_lt _ _
+  theorem sub_lt_sub_of_lt_of_le : ∀{a b c d : ℤ}, a < b → c ≤ d → a - d < b - c :=
+    @algebra.sub_lt_sub_of_lt_of_le _ _
+
+  theorem mul_le_mul_of_nonneg_left : ∀{a b c : ℤ}, a ≤ b → 0 ≤ c → c * a ≤ c * b :=
+    @algebra.mul_le_mul_of_nonneg_left _ _
+  theorem mul_le_mul_of_nonneg_right : ∀{a b c : ℤ}, a ≤ b → 0 ≤ c → a * c ≤ b * c :=
+    @algebra.mul_le_mul_of_nonneg_right _ _
+  theorem mul_le_mul : ∀{a b c d : ℤ}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d :=
+    @algebra.mul_le_mul _ _
+  theorem mul_nonpos_of_nonneg_of_nonpos : ∀{a b : ℤ}, a ≥ 0 → b ≤ 0 → a * b ≤ 0 :=
+    @algebra.mul_nonpos_of_nonneg_of_nonpos _ _
+  theorem mul_nonpos_of_nonpos_of_nonneg : ∀{a b : ℤ}, a ≤ 0 → b ≥ 0 → a * b ≤ 0 :=
+    @algebra.mul_nonpos_of_nonpos_of_nonneg _ _
+  theorem mul_lt_mul_of_pos_left : ∀{a b c : ℤ}, a < b → 0 < c → c * a < c * b :=
+    @algebra.mul_lt_mul_of_pos_left _ _
+  theorem mul_lt_mul_of_pos_right : ∀{a b c : ℤ}, a < b → 0 < c → a * c < b * c :=
+    @algebra.mul_lt_mul_of_pos_right _ _
+  theorem mul_lt_mul : ∀{a b c d : ℤ}, a < c → b ≤ d → 0 < b → 0 ≤ c → a * b < c * d :=
+    @algebra.mul_lt_mul _ _
+  theorem mul_neg_of_pos_of_neg : ∀{a b : ℤ}, a > 0 → b < 0 → a * b < 0 :=
+    @algebra.mul_neg_of_pos_of_neg _ _
+  theorem mul_neg_of_neg_of_pos : ∀{a b : ℤ}, a < 0 → b > 0 → a * b < 0 :=
+    @algebra.mul_neg_of_neg_of_pos _ _
+  theorem lt_of_mul_lt_mul_left : ∀{a b c : ℤ}, c * a < c * b → c ≥ zero → a < b :=
+    @algebra.lt_of_mul_lt_mul_left int _
+  theorem lt_of_mul_lt_mul_right : ∀{a b c : ℤ}, a * c < b * c → c ≥ 0 → a < b :=
+    @algebra.lt_of_mul_lt_mul_right _ _
+  theorem le_of_mul_le_mul_left : ∀{a b c : ℤ}, c * a ≤ c * b → c > 0 → a ≤ b :=
+    @algebra.le_of_mul_le_mul_left _ _
+  theorem le_of_mul_le_mul_right : ∀{a b c : ℤ}, a * c ≤ b * c → c > 0 → a ≤ b :=
+    @algebra.le_of_mul_le_mul_right _ _
+  theorem pos_of_mul_pos_left : ∀{a b : ℤ}, 0 < a * b → 0 ≤ a → 0 < b :=
+    @algebra.pos_of_mul_pos_left _ _
+  theorem pos_of_mul_pos_right : ∀{a b : ℤ}, 0 < a * b → 0 ≤ b → 0 < a :=
+    @algebra.pos_of_mul_pos_right _ _
+
+  theorem mul_le_mul_of_nonpos_left : ∀{a b c : ℤ}, b ≤ a → c ≤ 0 → c * a ≤ c * b :=
+    @algebra.mul_le_mul_of_nonpos_left _ _
+  theorem mul_le_mul_of_nonpos_right : ∀{a b c : ℤ}, b ≤ a → c ≤ 0 → a * c ≤ b * c :=
+    @algebra.mul_le_mul_of_nonpos_right _ _
+  theorem mul_nonneg_of_nonpos_of_nonpos : ∀{a b : ℤ}, a ≤ 0 → b ≤ 0 → 0 ≤ a * b :=
+    @algebra.mul_nonneg_of_nonpos_of_nonpos _ _
+  theorem mul_lt_mul_of_neg_left : ∀{a b c : ℤ}, b < a → c < 0 → c * a < c * b :=
+    @algebra.mul_lt_mul_of_neg_left _ _
+  theorem mul_lt_mul_of_neg_right : ∀{a b c : ℤ}, b < a → c < 0 → a * c < b * c :=
+    @algebra.mul_lt_mul_of_neg_right _ _
+  theorem mul_pos_of_neg_of_neg : ∀{a b : ℤ}, a < 0 → b < 0 → 0 < a * b :=
+    @algebra.mul_pos_of_neg_of_neg _ _
+
+  theorem mul_self_nonneg : ∀a : ℤ, a * a ≥ 0 := algebra.mul_self_nonneg
+  theorem zero_le_one : #int 0 ≤ 1 := @algebra.zero_le_one int int.linear_ordered_comm_ring
+  theorem zero_lt_one : #int 0 < 1 := @algebra.zero_lt_one int int.linear_ordered_comm_ring
+  theorem pos_and_pos_or_neg_and_neg_of_mul_pos : ∀{a b : ℤ}, a * b > 0 →
+    (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) := @algebra.pos_and_pos_or_neg_and_neg_of_mul_pos _ _
+end port_algebra
+
+/- more facts specific to int -/
+
+theorem nonneg_of_nat (n : ℕ) : 0 ≤ of_nat n := trivial
+
+theorem exists_eq_of_nat {a : ℤ} (H : 0 ≤ a) : ∃n : ℕ, a = of_nat n :=
+obtain (n : ℕ) (H1 : 0 + of_nat n = a), from le.elim H,
+exists.intro n (!zero_add ▸ (H1⁻¹))
+
+theorem exists_eq_neg_of_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -(of_nat n) :=
+have H2 : -a ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H,
+obtain (n : ℕ) (Hn : -a = of_nat n), from exists_eq_of_nat H2,
+exists.intro n (eq_neg_of_eq_neg (Hn⁻¹))
+
+theorem of_nat_nat_abs_of_nonneg {a : ℤ} (H : a ≥ 0) : of_nat (nat_abs a) = a :=
+obtain (n : ℕ) (Hn : a = of_nat n), from exists_eq_of_nat H,
+Hn⁻¹ ▸ congr_arg of_nat (nat_abs_of_nat n)
+
+theorem of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) : of_nat (nat_abs a) = -a :=
+have H1 : (-a) ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H,
+calc
+  of_nat (nat_abs a) = of_nat (nat_abs (-a)) : nat_abs_neg
+                 ... = -a                    : of_nat_nat_abs_of_nonneg H1
+
+exit
+
+
+
+
+
+
+
+
+
+
+
+-- ### interaction with add
+
+theorem le_add_of_nat_right (a : ℤ) (n : ℕ) : a ≤ a + n :=
+le.intro (eq.refl (a + n))
+
+theorem le_add_of_nat_left (a : ℤ) (n : ℕ) : a ≤ n + a :=
+le.intro (add.comm a n)
+
 
 theorem add_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a + c ≤ b + c :=
-add.comm c b ▸ add.comm c a ▸ add_le_left H c
+add.comm c b ▸ add.comm c a ▸ add_le_add_left H c
 
 theorem add_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : c ≤ d) : a + c ≤ b + d :=
-le_trans (add_le_right H1 c) (add_le_left H2 b)
+le_trans (add_le_right H1 c) (add_le_add_left H2 b)
 
 theorem add_le_cancel_right {a b c : ℤ} (H : a + c ≤ b + c) : a ≤ b :=
 have H1 : a + c + -c ≤ b + c + -c, from add_le_right H (-c),
@@ -118,7 +516,7 @@ theorem add_le_cancel_left {a b c : ℤ} (H : c + a ≤ c + b) : a ≤ b :=
 add_le_cancel_right (add.comm c b ▸ add.comm c a ▸ H)
 
 theorem add_le_inv {a b c d : ℤ} (H1 : a + b ≤ c + d) (H2 : c ≤ a) : b ≤ d :=
-obtain (n : ℕ) (Hn : c + n = a), from le_elim H2,
+obtain (n : ℕ) (Hn : c + n = a), from le.elim H2,
 have H3 : c + (n + b) ≤ c + d, from add.assoc c n b ▸ Hn⁻¹ ▸ H1,
 have H4 : n + b ≤ d, from add_le_cancel_left H3,
 show b ≤ d, from le_trans (le_add_of_nat_left b n) H4
@@ -127,7 +525,7 @@ theorem le_add_of_nat_right_trans {a b : ℤ} (H : a ≤ b) (n : ℕ) : a ≤ b
 le_trans H (le_add_of_nat_right b n)
 
 theorem le_imp_succ_le_or_eq {a b : ℤ} (H : a ≤ b) : a + 1 ≤ b ∨ a = b :=
-obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
+obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
 discriminate
   (assume H2 : n = 0,
     have H3 : a = b, from
@@ -143,19 +541,19 @@ discriminate
         a + 1 + k = a + succ k : by simp
           ... = a + n : by simp
           ... = b : Hn,
-    or.inl (le_intro H3))
+    or.inl (le.intro H3))
 
 -- ### interaction with neg and sub
 
 theorem le_neg {a b : ℤ} (H : a ≤ b) : -b ≤ -a :=
-obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
+obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
 have H2 : b - n = a, from (iff.mp !add_eq_iff_eq_add_neg Hn)⁻¹,
 have H3 : -b + n = -a, from
   calc
     -b + n = -b + -(-n) : {(neg_neg n)⁻¹}
       ... = -(b + -n) : (neg_add_distrib b (-n))⁻¹
       ... = -a : {H2},
-le_intro H3
+le.intro H3
 
 theorem neg_le_zero {a : ℤ} (H : 0 ≤ a) : -a ≤ 0 :=
 neg_zero ▸ (le_neg H)
@@ -167,13 +565,13 @@ theorem le_neg_inv {a b : ℤ} (H : -a ≤ -b) : b ≤ a :=
 neg_neg b ▸ neg_neg a ▸ le_neg H
 
 theorem le_sub_of_nat (a : ℤ) (n : ℕ) : a - n ≤ a :=
-le_intro (neg_add_cancel_right a n)
+le.intro (neg_add_cancel_right a n)
 
 theorem sub_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a - c ≤ b - c :=
 add_le_right H _
 
 theorem sub_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c - b ≤ c - a :=
-add_le_left (le_neg H) _
+add_le_add_left (le_neg H) _
 
 theorem sub_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : d ≤ c) : a - c ≤ b - d :=
 add_le H1 (le_neg H2)
@@ -213,59 +611,14 @@ iff.refl (n ≥ m)
 
 -- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2
 
-theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n :=
-le_intro (show a + 1 + n = a + succ n, by simp)
-
-theorem lt_intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b :=
-H ▸ lt_add_succ a n
-
-theorem lt_elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b :=
-obtain (n : ℕ) (Hn : a + 1 + n = b), from le_elim H,
-have H2 : a + succ n = b, from
-  calc
-    a + succ n = a + 1 + n : by simp
-      ... = b : Hn,
-exists.intro n H2
 
 -- -- ### basic facts
 
-theorem lt_irrefl (a : ℤ) : ¬ a < a :=
-(assume H : a < a,
-  obtain (n : ℕ) (Hn : a + succ n = a), from lt_elim H,
-  have H2 : a + succ n = a + 0, from
-    calc
-      a + succ n = a : Hn
-        ... = a + 0 : by simp,
-  have H3 : succ n = 0, from add.left_cancel H2,
-  have H4 : succ n = 0, from of_nat_inj H3,
-  absurd H4 !succ_ne_zero)
-
-theorem lt_imp_ne {a b : ℤ} (H : a < b) : a ≠ b :=
-(assume H2 : a = b, absurd (H2 ▸ H) (lt_irrefl b))
-
-theorem lt_of_nat (n m : ℕ) : (of_nat n < of_nat m) ↔ (n < m) :=
-calc
-  (of_nat n + 1 ≤ of_nat m) ↔ (of_nat (succ n) ≤ of_nat m) : by simp
-    ... ↔ (succ n ≤ m) : le_of_nat (succ n) m
-    ... ↔ (n < m) : iff.symm (nat.lt_def n m)
-
 theorem gt_of_nat (n m : ℕ) : (of_nat n > of_nat m) ↔ (n > m) :=
-lt_of_nat m n
+of_nat_lt_of_nat m n
 
 -- ### interaction with le
 
-theorem lt_imp_le_succ {a b : ℤ} (H : a < b) : a + 1 ≤ b :=
-H
-
-theorem le_succ_imp_lt {a b : ℤ} (H : a + 1 ≤ b) : a < b :=
-H
-
-theorem self_lt_succ (a : ℤ) : a < a + 1 :=
-le_refl (a + 1)
-
-theorem lt_imp_le {a b : ℤ} (H : a < b) : a ≤ b :=
-obtain (n : ℕ) (Hn : a + succ n = b), from lt_elim H,
-le_intro Hn
 
 theorem le_imp_lt_or_eq {a b : ℤ} (H : a ≤ b) : a < b ∨ a = b :=
 le_imp_succ_le_or_eq H
@@ -289,22 +642,22 @@ theorem le_lt_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b < c) : a < c :=
 le_trans (add_le_right H1 1) H2
 
 theorem lt_trans {a b c : ℤ} (H1 : a < b) (H2 : b < c) : a < c :=
-lt_le_trans H1 (lt_imp_le H2)
+lt_le_trans H1 (le_of_lt H2)
 
 theorem le_imp_not_gt {a b : ℤ} (H : a ≤ b) : ¬ a > b :=
-(assume H2 : a > b, absurd (le_lt_trans H H2) (lt_irrefl a))
+(assume H2 : a > b, absurd (le_lt_trans H H2) (lt.irrefl a))
 
 theorem lt_imp_not_ge {a b : ℤ} (H : a < b) : ¬ a ≥ b :=
-(assume H2 : a ≥ b, absurd (lt_le_trans H H2) (lt_irrefl a))
+(assume H2 : a ≥ b, absurd (lt_le_trans H H2) (lt.irrefl a))
 
 theorem lt_antisym {a b : ℤ} (H : a < b) : ¬ b < a :=
-le_imp_not_gt (lt_imp_le H)
+le_imp_not_gt (le_of_lt H)
 
 -- ### interaction with addition
 
 -- TODO: note: no longer works without the "show"
 theorem add_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b :=
-show (c + a) + 1 ≤ c + b, from (add.assoc c a 1)⁻¹ ▸ add_le_left H c
+show (c + a) + 1 ≤ c + b, from (add.assoc c a 1)⁻¹ ▸ add_le_add_left H c
 
 theorem add_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a + c < b + c :=
 add.comm c b ▸ add.comm c a ▸ add_lt_left H c
@@ -313,10 +666,10 @@ theorem add_le_lt {a b c d : ℤ} (H1 : a ≤ c) (H2 : b < d) : a + b < c + d :=
 le_lt_trans (add_le_right H1 b) (add_lt_left H2 c)
 
 theorem add_lt_le {a b c d : ℤ} (H1 : a < c) (H2 : b ≤ d) : a + b < c + d :=
-lt_le_trans (add_lt_right H1 b) (add_le_left H2 c)
+lt_le_trans (add_lt_right H1 b) (add_le_add_left H2 c)
 
 theorem add_lt {a b c d : ℤ} (H1 : a < c) (H2 : b < d) : a + b < c + d :=
-add_lt_le H1 (lt_imp_le H2)
+add_lt_le H1 (le_of_lt H2)
 
 theorem add_lt_cancel_left {a b c : ℤ} (H : c + a < c + b) : a < b :=
 show a + 1 ≤ b, from add_le_cancel_left (add.assoc c a 1 ▸ H)
@@ -342,7 +695,7 @@ theorem lt_neg_inv {a b : ℤ} (H : -a < -b) : b < a :=
 neg_neg b ▸ neg_neg a ▸ lt_neg H
 
 theorem lt_sub_of_nat_succ (a : ℤ) (n : ℕ) : a - succ n < a :=
-lt_intro (neg_add_cancel_right a (succ n))
+lt.intro (neg_add_cancel_right a (succ n))
 
 theorem sub_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a - c < b - c :=
 add_lt_right H _
@@ -375,10 +728,15 @@ by_cases_of_nat a
   (take n : ℕ,
     by_cases_of_nat_succ b
       (take m : ℕ,
-        show of_nat n ≤ m ∨ of_nat n > m, by simp) -- from (by simp) ◂ (le_or_gt n m))
+        show of_nat n ≤ m ∨ of_nat n > m, from
+        proof
+          or.elim (@nat.le_or_gt n m)
+            (assume H : n ≤ m, or.inl (iff.mp' !of_nat_le_of_nat H))
+            (assume H : n > m, or.inr (iff.mp' !of_nat_lt_of_nat H))
+        qed)
       (take m : ℕ,
         show n ≤ -succ m ∨ n > -succ m, from
-          have H0 : -succ m < -m, from lt_neg ((of_nat_succ m)⁻¹ ▸ self_lt_succ m),
+          have H0 : -succ m < -m, from lt_neg ((of_nat_succ m)⁻¹ ▸ lt_succ m),
           have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n),
           or.inr H))
   (take n : ℕ,
@@ -390,9 +748,9 @@ by_cases_of_nat a
          show -n ≤ -succ m ∨ -n > -succ m, from
           or_of_or_of_imp_of_imp le_or_gt
             (assume H : succ m ≤ n,
-              le_neg (iff.elim_left (iff.symm (le_of_nat (succ m) n)) H))
+              le_neg (iff.elim_left (iff.symm (of_nat_le_of_nat (succ m) n)) H))
             (assume H : succ m > n,
-              lt_neg (iff.elim_left (iff.symm (lt_of_nat n (succ m))) H))))
+              lt_neg (iff.elim_left (iff.symm (of_nat_lt_of_nat n (succ m))) H))))
 
 theorem trichotomy_alt (a b : ℤ) : (a < b ∨ a = b) ∨ a > b :=
 or_of_or_of_imp_left (le_or_gt a b) (assume H : a ≤ b, le_imp_lt_or_eq H)
@@ -401,9 +759,9 @@ theorem trichotomy (a b : ℤ) : a < b ∨ a = b ∨ a > b :=
 iff.elim_left or.assoc (trichotomy_alt a b)
 
 theorem le_total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
-or_of_or_of_imp_right (le_or_gt a b) (assume H : b < a, lt_imp_le H)
+or_of_or_of_imp_right (le_or_gt a b) (assume H : b < a, le_of_lt H)
 
-theorem not_lt_imp_le {a b : ℤ} (H : ¬ a < b) : b ≤ a :=
+theorem not_le_of_lt {a b : ℤ} (H : ¬ a < b) : b ≤ a :=
 or_resolve_left (le_or_gt b a) H
 
 theorem not_le_imp_lt {a b : ℤ} (H : ¬ a ≤ b) : b < a :=
@@ -417,7 +775,7 @@ or_resolve_right (le_or_gt a b) H
 -- see also "int_by_cases" and similar theorems
 
 theorem pos_imp_exists_nat {a : ℤ} (H : a ≥ 0) : ∃n : ℕ, a = n :=
-obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le_elim H,
+obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le.elim H,
 exists.intro n (Hn⁻¹ ⬝ zero_add n)
 
 theorem neg_imp_exists_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n :=
@@ -431,7 +789,7 @@ obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H,
 Hn⁻¹ ▸ congr_arg of_nat (nat_abs_of_nat n)
 
 theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
-iff.mp (iff.symm !le_of_nat) !zero_le
+iff.mp (iff.symm !of_nat_le_of_nat) !zero_le
 
 definition ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) := _
 definition lt_decidable [instance] {a b : ℤ} : decidable (a < b) := _
@@ -454,14 +812,14 @@ or_of_or_of_imp_of_imp (le_total 0 a)
 -- ### interaction of mul with le and lt
 
 theorem mul_le_left_nonneg {a b c : ℤ} (Ha : a ≥ 0) (H : b ≤ c) : a * b ≤ a * c :=
-obtain (n : ℕ) (Hn : b + n = c), from le_elim H,
+obtain (n : ℕ) (Hn : b + n = c), from le.elim H,
 have H2 : a * b + of_nat ((nat_abs a) * n) = a * c, from
   calc
     a * b + of_nat ((nat_abs a) * n) = a * b + (nat_abs a) * of_nat n : by simp
       ... = a * b + a * n : {nat_abs_nonneg_eq Ha}
       ... = a * (b + n) : by simp
       ... = a * c : by simp,
-le_intro H2
+le.intro H2
 
 theorem mul_le_right_nonneg {a b c : ℤ} (Hb : b ≥ 0) (H : a ≤ c) : a * b ≤ c * b :=
 !mul.comm ▸ !mul.comm ▸ mul_le_left_nonneg Hb H
@@ -479,13 +837,13 @@ theorem mul_le_nonneg {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) (Hc : a ≤
   : a * b ≤ c * d :=
 le_trans (mul_le_right_nonneg Hb Hc) (mul_le_left_nonneg (le_trans Ha Hc) Hd)
 
-theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb : b ≤ 0) (Hc : c ≤ a) (Hd : d ≤ b)
+theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb :b ≤ 0) (Hc : c ≤ a) (Hd : d ≤ b)
   : a * b ≤ c * d :=
 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_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,
+have H3 : a * b + a ≤ a * c, from (by simp) ▸ mul_le_left_nonneg (le_of_lt Ha) H,
 lt_le_trans H2 H3
 
 theorem mul_lt_right_pos {a b c : ℤ} (Hb : b > 0) (H : a < c) : a * b < c * b :=
@@ -505,11 +863,11 @@ le_lt_trans (mul_le_right_nonneg Hb Hc) (mul_lt_left_pos (lt_le_trans Ha Hc) Hd)
 
 theorem mul_lt_le_pos {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b > 0) (Hc : a < c) (Hd : b ≤ d)
   : a * b < c * d :=
-lt_le_trans (mul_lt_right_pos Hb Hc) (mul_le_left_nonneg (le_trans Ha (lt_imp_le Hc)) Hd)
+lt_le_trans (mul_lt_right_pos Hb Hc) (mul_le_left_nonneg (le_trans Ha (le_of_lt Hc)) Hd)
 
 theorem mul_lt_pos {a b c d : ℤ} (Ha : a > 0) (Hb : b > 0) (Hc : a < c) (Hd : b < d)
   : a * b < c * d :=
-mul_lt_le_pos (lt_imp_le Ha) Hb Hc (lt_imp_le Hd)
+mul_lt_le_pos (le_of_lt Ha) Hb Hc (le_of_lt Hd)
 
 theorem mul_lt_neg {a b c d : ℤ} (Ha : a < 0) (Hb : b < 0) (Hc : c < a) (Hd : d < b)
   : a * b < c * d :=
@@ -583,13 +941,13 @@ theorem sign_negative {a : ℤ} (H : a < 0) : sign a = - 1 :=
 if_neg (lt_antisym H) ⬝ if_pos H
 
 theorem sign_zero : sign 0 = 0 :=
-if_neg (lt_irrefl 0) ⬝ if_neg (lt_irrefl 0)
+if_neg (lt.irrefl 0) ⬝ if_neg (lt.irrefl 0)
 
 -- add_rewrite sign_negative sign_pos nat_abs_negative nat_abs_nonneg_eq sign_zero mul_nat_abs
 
 theorem mul_sign_nat_abs (a : ℤ) : sign a * (nat_abs a) = a :=
-have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le,
-have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, lt_imp_le,
+have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, le_of_lt,
+have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, le_of_lt,
 or.elim3 (trichotomy a 0)
   (assume H : a < 0, by simp)
   (assume H : a = 0, by simp)
@@ -615,7 +973,7 @@ or.elim (em (a = 0))
         mul.cancel_right H3 H))
 
 theorem sign_idempotent (a : ℤ) : sign (sign a) = sign a :=
-have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (lt_of_nat 0 1)) !succ_pos,
+have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (of_nat_lt_of_nat 0 1)) !succ_pos,
     --this should be done with simp
 or.elim3 (trichotomy a 0) sorry sorry sorry
 --  (by simp)
@@ -623,7 +981,7 @@ or.elim3 (trichotomy a 0) sorry sorry sorry
 --  (by simp)
 
 theorem sign_succ (n : ℕ) : sign (succ n) = 1 :=
-sign_pos (iff.elim_left (iff.symm (lt_of_nat 0 (succ n))) !succ_pos)
+sign_pos (iff.elim_left (iff.symm (of_nat_lt_of_nat 0 (succ n))) !succ_pos)
   --this should be done with simp
 
 theorem sign_neg (a : ℤ) : sign (-a) = - sign a :=
@@ -644,8 +1002,8 @@ or.elim3 (trichotomy a 0) sorry
 --  (by simp)
 
 theorem sign_nat_abs (a : ℤ) : sign (nat_abs a) = nat_abs (sign a) :=
-have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le,
-have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, lt_imp_le,
+have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, le_of_lt,
+have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, le_of_lt,
 or.elim3 (trichotomy a 0) sorry sorry sorry
 --  (by simp)
 --  (by simp)
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 86a0e89cf..b5ac3d461 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -65,6 +65,9 @@ induction_on n
   (take m IH, or.inr
     (show succ m = succ (pred (succ m)), from congr_arg succ !pred.succ⁻¹))
 
+theorem exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : ∃k : ℕ, n = succ k :=
+exists.intro _ (or_resolve_right !eq_zero_or_eq_succ_pred H)
+
 theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
 no_confusion H (λe, e)
 
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 8586c567e..fec040e52 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -13,6 +13,10 @@ open eq.ops
 
 namespace nat
 
+-- TODO: move this
+theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
+iff.intro succ_le_of_lt lt_of_succ_le
+
 -- Less than or equal
 -- ------------------