diff --git a/algebra/big_operators.lean b/algebra/big_operators.lean
index 3d5caa0800e33..51804cfec7a7c 100644
--- a/algebra/big_operators.lean
+++ b/algebra/big_operators.lean
@@ -161,9 +161,7 @@ end finset
 run_cmd transport_multiplicative_to_additive [
   /- map operations -/
   (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg),
-  (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg),
-  /- map constructors -/
-  (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk),
+  (`has_one, `has_zero), (`has_mul, `has_add), (`has_inv, `has_neg),
   /- map structures -/
   (`semigroup, `add_semigroup),
   (`monoid, `add_monoid),
@@ -190,16 +188,6 @@ run_cmd transport_multiplicative_to_additive [
   (`comm_group.to_comm_monoid, `add_comm_group.to_add_comm_monoid),
   (`left_cancel_semigroup.to_semigroup, `add_left_cancel_semigroup.to_add_semigroup),
   (`right_cancel_semigroup.to_semigroup, `add_right_cancel_semigroup.to_add_semigroup),
-  /- map projections -/
-  (`semigroup.mul_assoc, `add_semigroup.add_assoc),
-  (`comm_semigroup.mul_comm, `add_comm_semigroup.add_comm),
-  (`left_cancel_semigroup.mul_left_cancel, `add_left_cancel_semigroup.add_left_cancel),
-  (`right_cancel_semigroup.mul_right_cancel, `add_right_cancel_semigroup.add_right_cancel),
-  (`monoid.one_mul, `add_monoid.zero_add),
-  (`monoid.mul_one, `add_monoid.add_zero),
-  (`group.mul_left_inv, `add_group.add_left_neg),
-  (`group.mul, `add_group.add),
-  (`group.mul_assoc, `add_group.add_assoc),
   /- map lemmas -/
   (`mul_assoc, `add_assoc),
   (`mul_comm, `add_comm),
@@ -210,45 +198,16 @@ run_cmd transport_multiplicative_to_additive [
   (`mul_left_inv, `add_left_neg),
   (`mul_left_cancel, `add_left_cancel),
   (`mul_right_cancel, `add_right_cancel),
-  (`mul_left_cancel_iff, `add_left_cancel_iff),
-  (`mul_right_cancel_iff, `add_right_cancel_iff),
   (`inv_mul_cancel_left, `neg_add_cancel_left),
   (`inv_mul_cancel_right, `neg_add_cancel_right),
-  (`eq_inv_mul_of_mul_eq, `eq_neg_add_of_add_eq),
-  (`inv_eq_of_mul_eq_one, `neg_eq_of_add_eq_zero),
   (`inv_inv, `neg_neg),
-  (`mul_right_inv, `add_right_neg),
   (`mul_inv_cancel_left, `add_neg_cancel_left),
   (`mul_inv_cancel_right, `add_neg_cancel_right),
-  (`mul_inv_rev, `neg_add_rev),
   (`mul_inv, `neg_add),
-  (`inv_inj, `neg_inj),
-  (`group.mul_left_cancel, `add_group.add_left_cancel),
-  (`group.mul_right_cancel, `add_group.add_right_cancel),
-  (`group.to_left_cancel_semigroup, `add_group.to_left_cancel_add_semigroup),
   (`group.to_right_cancel_semigroup, `add_group.to_right_cancel_add_semigroup),
   (`eq_inv_of_eq_inv, `eq_neg_of_eq_neg),
-  (`eq_inv_of_mul_eq_one, `eq_neg_of_add_eq_zero),
-  (`eq_mul_inv_of_mul_eq, `eq_add_neg_of_add_eq),
-  (`inv_mul_eq_of_eq_mul, `neg_add_eq_of_eq_add),
-  (`mul_inv_eq_of_eq_mul, `add_neg_eq_of_eq_add),
-  (`eq_mul_of_mul_inv_eq, `eq_add_of_add_neg_eq),
-  (`eq_mul_of_inv_mul_eq, `eq_add_of_neg_add_eq),
-  (`mul_eq_of_eq_inv_mul, `add_eq_of_eq_neg_add),
-  (`mul_eq_of_eq_mul_inv, `add_eq_of_eq_add_neg),
   (`one_inv, `neg_zero),
-  (`left_inverse_inv, `left_inverse_neg),
-  (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq),
-  (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero),
-  (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero),
-  (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg),
-  (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero),
-  (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add),
-  (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg),
-  -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero)   not needed for commutative groups
-  -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero)
-
-  --NEW:
+  /- new lemmas -/
   (`list.prod, `list.sum),
   (`list.prod.equations._eqn_1, `list.sum.equations._eqn_1),
   (`list.prod_nil, `list.sum_nil),
diff --git a/algebra/functions.lean b/algebra/functions.lean
new file mode 100644
index 0000000000000..5368e3bea27cf
--- /dev/null
+++ b/algebra/functions.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+
+universe u
+variables {α : Type u}
+
+section
+variables [decidable_linear_order α] {a b c : α}
+
+lemma le_min_iff : c ≤ min a b ↔ c ≤ a ∧ c ≤ b :=
+⟨λ h, ⟨le_trans h (min_le_left a b), le_trans h (min_le_right a b)⟩,
+ λ ⟨h₁, h₂⟩, le_min h₁ h₂⟩
+
+lemma max_le_iff : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
+⟨λ h, ⟨le_trans (le_max_left a b) h, le_trans (le_max_right a b) h⟩,
+ λ ⟨h₁, h₂⟩, max_le h₁ h₂⟩
+
+end
+
+section decidable_linear_ordered_comm_group
+variables [decidable_linear_ordered_comm_group α] {a b : α}
+
+theorem abs_le : abs a ≤ b ↔ (- b ≤ a ∧ a ≤ b) :=
+⟨assume h, ⟨neg_le_of_neg_le $ le_trans (neg_le_abs_self _) h, le_trans (le_abs_self _) h⟩,
+  assume ⟨h₁, h₂⟩, abs_le_of_le_of_neg_le h₂ $ neg_le_of_neg_le h₁⟩
+
+lemma abs_lt : abs a < b ↔ (- b < a ∧ a < b) :=
+⟨assume h, ⟨neg_lt_of_neg_lt $ lt_of_le_of_lt (neg_le_abs_self _) h, lt_of_le_of_lt (le_abs_self _) h⟩,
+  assume ⟨h₁, h₂⟩, abs_lt_of_lt_of_neg_lt h₂ $ neg_lt_of_neg_lt h₁⟩
+
+@[simp] lemma abs_eq_zero : abs a = 0 ↔ a = 0 :=
+⟨eq_zero_of_abs_eq_zero, λ e, e.symm ▸ abs_zero⟩
+
+end decidable_linear_ordered_comm_group
diff --git a/algebra/group.lean b/algebra/group.lean
index 601d2b42394e0..c020c11954ff1 100644
--- a/algebra/group.lean
+++ b/algebra/group.lean
@@ -8,148 +8,142 @@ Various multiplicative and additive structures.
 universe variable u
 variable {α : Type u}
 
+@[simp] theorem mul_left_inj [left_cancel_semigroup α] {a b c : α} : a * b = a * c ↔ b = c :=
+⟨mul_left_cancel, congr_arg _⟩
+
+@[simp] theorem mul_right_inj [right_cancel_semigroup α] {a b c : α} : b * a = c * a ↔ b = c :=
+⟨mul_right_cancel, congr_arg _⟩
+
 section group
-  variable [group α]
+  variables [group α] {a b c : α}
+
+  @[simp] theorem inv_inj' : a⁻¹ = b⁻¹ ↔ a = b :=
+  ⟨λ h, by rw ← inv_inv a; simp [h], congr_arg _⟩
+
+  theorem eq_of_inv_eq_inv : a⁻¹ = b⁻¹ → a = b :=
+  inv_inj'.1
+
+  @[simp] theorem mul_self_iff_eq_one : a * a = a ↔ a = 1 :=
+  by have := @mul_left_inj _ _ a a 1; rwa mul_one at this
+
+  @[simp] theorem inv_eq_one : a⁻¹ = 1 ↔ a = 1 :=
+  by rw [← @inv_inj' _ _ a 1, one_inv]
+
+  @[simp] theorem inv_ne_one : a⁻¹ ≠ 1 ↔ a ≠ 1 :=
+  not_congr inv_eq_one
 
-  variable (α)
-  theorem left_inverse_inv : function.left_inverse (λ a : α, a⁻¹) (λ a, a⁻¹) :=
+  theorem left_inverse_inv (α) [group α] :
+    function.left_inverse (λ a : α, a⁻¹) (λ a, a⁻¹) :=
   assume a, inv_inv a
-  variable {α}
 
-  theorem inv_eq_inv_iff_eq (a b : α) : a⁻¹ = b⁻¹ ↔ a = b :=
-  iff.intro inv_inj (begin intro h, simp [h] end)
+  attribute [simp] mul_inv_cancel_left mul_inv_cancel_right
 
-  theorem inv_eq_one_iff_eq_one (a : α) : a⁻¹ = 1 ↔ a = 1 :=
-  have a⁻¹ = 1⁻¹ ↔ a = 1, from inv_eq_inv_iff_eq a 1,
-  begin rewrite this.symm, simp end
+  theorem eq_inv_iff_eq_inv : a = b⁻¹ ↔ b = a⁻¹ :=
+  ⟨eq_inv_of_eq_inv, eq_inv_of_eq_inv⟩
 
-  theorem eq_one_of_inv_eq_one (a : α) : a⁻¹ = 1 → a = 1 :=
-  iff.mp (inv_eq_one_iff_eq_one a)
+  theorem inv_eq_iff_inv_eq : a⁻¹ = b ↔ b⁻¹ = a :=
+  by rw [eq_comm, @eq_comm _ _ a, eq_inv_iff_eq_inv]
 
-  theorem eq_inv_iff_eq_inv (a b : α) : a = b⁻¹ ↔ b = a⁻¹ :=
-  iff.intro eq_inv_of_eq_inv eq_inv_of_eq_inv
+  theorem mul_eq_one_iff_eq_inv : a * b = 1 ↔ a = b⁻¹ :=
+  have a * b = b⁻¹ * b ↔ a = b⁻¹, from mul_right_inj,
+  by rwa mul_left_inv at this
 
-  theorem eq_of_mul_inv_eq_one {a b : α} (H : a * b⁻¹ = 1) : a = b :=
-  calc
-    a    = a * b⁻¹ * b : by simp
-     ... = b           : begin rewrite H, simp end
+  theorem mul_eq_one_iff_inv_eq : a * b = 1 ↔ a⁻¹ = b :=
+  by rw [mul_eq_one_iff_eq_inv, eq_inv_iff_eq_inv, eq_comm]
 
-  theorem mul_eq_iff_eq_inv_mul (a b c : α) : a * b = c ↔ b = a⁻¹ * c :=
-  iff.intro eq_inv_mul_of_mul_eq mul_eq_of_eq_inv_mul
+  @[simp] theorem eq_mul_inv_iff_mul_eq : a = b * c⁻¹ ↔ a * c = b :=
+  ⟨λ h, by simp [h], λ h, by simp [h.symm]⟩
 
-  theorem mul_eq_iff_eq_mul_inv (a b c : α) : a * b = c ↔ a = c * b⁻¹ :=
-  iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv
+  @[simp] theorem eq_inv_mul_iff_mul_eq : a = b⁻¹ * c ↔ b * a = c :=
+  ⟨λ h, by simp [h], λ h, by simp [h.symm]⟩
+
+  @[simp] theorem inv_mul_eq_iff_eq_mul : a⁻¹ * b = c ↔ b = a * c :=
+  ⟨λ h, by simp [h.symm], λ h, by simp [h]⟩
+
+  @[simp] theorem mul_inv_eq_iff_eq_mul : a * b⁻¹ = c ↔ a = c * b :=
+  ⟨λ h, by simp [h.symm], λ h, by simp [h]⟩
+
+  theorem mul_inv_eq_one {a b : α} : a * b⁻¹ = 1 ↔ a = b :=
+  by rw [mul_eq_one_iff_eq_inv, inv_inv]
 end group
 
 /- transport versions to additive -/
 run_cmd transport_multiplicative_to_additive [
   /- map operations -/
   (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg),
-  (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg),
-  /- map constructors -/
-  (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk),
+  (`has_mul, `has_add), (`has_inv, `has_neg),
   /- map structures -/
-  (`semigroup, `add_semigroup),
-  (`monoid, `add_monoid),
   (`group, `add_group),
-  (`comm_semigroup, `add_comm_semigroup),
-  (`comm_monoid, `add_comm_monoid),
-  (`comm_group, `add_comm_group),
   (`left_cancel_semigroup, `add_left_cancel_semigroup),
   (`right_cancel_semigroup, `add_right_cancel_semigroup),
-  (`left_cancel_semigroup.mk, `add_left_cancel_semigroup.mk),
-  (`right_cancel_semigroup.mk, `add_right_cancel_semigroup.mk),
   /- map instances -/
   (`semigroup.to_has_mul, `add_semigroup.to_has_add),
   (`monoid.to_has_one, `add_monoid.to_has_zero),
   (`group.to_has_inv, `add_group.to_has_neg),
-  (`comm_semigroup.to_semigroup, `add_comm_semigroup.to_add_semigroup),
   (`monoid.to_semigroup, `add_monoid.to_add_semigroup),
-  (`comm_monoid.to_monoid, `add_comm_monoid.to_add_monoid),
-  (`comm_monoid.to_comm_semigroup, `add_comm_monoid.to_add_comm_semigroup),
   (`group.to_monoid, `add_group.to_add_monoid),
-  (`comm_group.to_group, `add_comm_group.to_add_group),
-  (`comm_group.to_comm_monoid, `add_comm_group.to_add_comm_monoid),
   (`left_cancel_semigroup.to_semigroup, `add_left_cancel_semigroup.to_add_semigroup),
   (`right_cancel_semigroup.to_semigroup, `add_right_cancel_semigroup.to_add_semigroup),
-  /- map projections -/
-  (`semigroup.mul_assoc, `add_semigroup.add_assoc),
-  (`comm_semigroup.mul_comm, `add_comm_semigroup.add_comm),
-  (`left_cancel_semigroup.mul_left_cancel, `add_left_cancel_semigroup.add_left_cancel),
-  (`right_cancel_semigroup.mul_right_cancel, `add_right_cancel_semigroup.add_right_cancel),
-  (`monoid.one_mul, `add_monoid.zero_add),
-  (`monoid.mul_one, `add_monoid.add_zero),
-  (`group.mul_left_inv, `add_group.add_left_neg),
-  (`group.mul, `add_group.add),
-  (`group.mul_assoc, `add_group.add_assoc),
   /- map lemmas -/
-  (`mul_assoc, `add_assoc),
-  (`mul_comm, `add_comm),
-  (`mul_left_comm, `add_left_comm),
-  (`mul_right_comm, `add_right_comm),
-  (`one_mul, `zero_add),
-  (`mul_one, `add_zero),
   (`mul_left_inv, `add_left_neg),
   (`mul_left_cancel, `add_left_cancel),
   (`mul_right_cancel, `add_right_cancel),
-  (`mul_left_cancel_iff, `add_left_cancel_iff),
-  (`mul_right_cancel_iff, `add_right_cancel_iff),
   (`inv_mul_cancel_left, `neg_add_cancel_left),
   (`inv_mul_cancel_right, `neg_add_cancel_right),
-  (`eq_inv_mul_of_mul_eq, `eq_neg_add_of_add_eq),
-  (`inv_eq_of_mul_eq_one, `neg_eq_of_add_eq_zero),
   (`inv_inv, `neg_neg),
-  (`mul_right_inv, `add_right_neg),
   (`mul_inv_cancel_left, `add_neg_cancel_left),
   (`mul_inv_cancel_right, `add_neg_cancel_right),
-  (`mul_inv_rev, `neg_add_rev),
-  (`mul_inv, `neg_add),
-  (`inv_inj, `neg_inj),
-  (`group.mul_left_cancel, `add_group.add_left_cancel),
-  (`group.mul_right_cancel, `add_group.add_right_cancel),
-  (`group.to_left_cancel_semigroup, `add_group.to_left_cancel_add_semigroup),
   (`group.to_right_cancel_semigroup, `add_group.to_right_cancel_add_semigroup),
   (`eq_inv_of_eq_inv, `eq_neg_of_eq_neg),
-  (`eq_inv_of_mul_eq_one, `eq_neg_of_add_eq_zero),
-  (`eq_mul_inv_of_mul_eq, `eq_add_neg_of_add_eq),
-  (`inv_mul_eq_of_eq_mul, `neg_add_eq_of_eq_add),
-  (`mul_inv_eq_of_eq_mul, `add_neg_eq_of_eq_add),
-  (`eq_mul_of_mul_inv_eq, `eq_add_of_add_neg_eq),
-  (`eq_mul_of_inv_mul_eq, `eq_add_of_neg_add_eq),
-  (`mul_eq_of_eq_inv_mul, `add_eq_of_eq_neg_add),
-  (`mul_eq_of_eq_mul_inv, `add_eq_of_eq_add_neg),
   (`one_inv, `neg_zero),
+  /- new lemmas -/
+  (`mul_left_inj, `add_left_inj),
+  (`mul_right_inj, `add_right_inj),
+  (`inv_inj', `neg_inj'),
+  (`inv_eq_one, `neg_eq_zero),
+  (`inv_ne_one, `neg_ne_zero),
   (`left_inverse_inv, `left_inverse_neg),
-  (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq),
-  (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero),
-  (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero),
   (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg),
-  (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero),
-  (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add),
-  (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg)
-  -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero)   not needed for commutative groups
-  -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero)
-  ]
+  (`inv_eq_iff_inv_eq, `neg_eq_iff_neg_eq),
+  (`mul_eq_one_iff_eq_inv, `add_eq_zero_iff_eq_neg),
+  (`mul_eq_one_iff_inv_eq, `add_eq_zero_iff_neg_eq),
+  (`eq_mul_inv_iff_mul_eq, `eq_add_neg_iff_add_eq),
+  (`eq_inv_mul_iff_mul_eq, `eq_neg_add_iff_add_eq),
+  (`inv_mul_eq_iff_eq_mul, `neg_add_eq_iff_eq_add),
+  (`mul_inv_eq_iff_eq_mul, `add_neg_eq_iff_eq_add),
+  (`mul_inv_eq_one, `add_neg_eq_zero)]
 
 section add_group
-  variable [add_group α]
+  variables [add_group α] {a b c : α}
 
   local attribute [simp] sub_eq_add_neg
 
-  theorem eq_iff_sub_eq_zero (a b : α) : a = b ↔ a - b = 0 :=
-  iff.intro (assume h, by simp [h]) (assume h, eq_of_sub_eq_zero h)
+  @[simp] lemma sub_left_inj : a - b = a - c ↔ b = c :=
+  add_left_inj.trans neg_inj'
+
+  @[simp] lemma sub_right_inj : b - a = c - a ↔ b = c :=
+  add_right_inj
+
+  lemma sub_add_sub_cancel (a b c : α) : (a - b) + (b - c) = a - c :=
+  by simp
+
+  lemma sub_sub_sub_cancel_right (a b c : α) : (a - c) - (b - c) = a - b :=
+  by simp
+
+  theorem sub_eq_zero : a - b = 0 ↔ a = b :=
+  ⟨eq_of_sub_eq_zero, λ h, by simp [h]⟩
 
-  theorem sub_eq_iff_eq_add (a b c : α) : a - b = c ↔ a = c + b :=
-  iff.intro (assume H, eq_add_of_add_neg_eq H) (assume H, add_neg_eq_of_eq_add H)
+  theorem sub_ne_zero : a - b ≠ 0 ↔ a ≠ b :=
+  not_congr sub_eq_zero
 
-  theorem eq_sub_iff_add_eq (a b c : α) : a = b - c ↔ a + c = b :=
-  iff.intro (assume H, add_eq_of_eq_add_neg H) (assume H, eq_add_neg_of_add_eq H)
+  @[simp] theorem eq_sub_iff_add_eq : a = b - c ↔ a + c = b :=
+  by split; intro h; simp [h]
+
+  theorem sub_eq_iff_eq_add : a - b = c ↔ a = c + b :=
+  by split; intro h; simp * at *
 
   theorem eq_iff_eq_of_sub_eq_sub {a b c d : α} (H : a - b = c - d) : a = b ↔ c = d :=
-  calc
-    a = b ↔ a - b = 0   : eq_iff_sub_eq_zero a b
-      ... = (c - d = 0) : by rewrite H
-      ... ↔ c = d       : iff.symm (eq_iff_sub_eq_zero c d)
+  by rw [← sub_eq_zero, H, sub_eq_zero]
 
   theorem left_inverse_sub_add_left (c : α) : function.left_inverse (λ x, x - c) (λ x, x + c) :=
   assume x, add_sub_cancel x c
@@ -166,135 +160,41 @@ section add_group
   assume x, neg_add_cancel_left c x
 end add_group
 
-section ordered_comm_group
-variables [ordered_comm_group α]
-
-lemma le_sub_iff_add_le {a b c : α} : a ≤ b - c ↔ a + c ≤ b :=
-by rw [add_comm]; exact ⟨add_le_of_le_sub_left, le_sub_left_of_add_le⟩
-
-lemma sub_le_iff_le_add {a b c : α} : a - c ≤ b ↔ a ≤ b + c :=
-by rw [add_comm]; exact ⟨le_add_of_sub_left_le, sub_left_le_of_le_add⟩
-
-end ordered_comm_group
-
-section decidable_linear_ordered_comm_group
-variables [decidable_linear_ordered_comm_group α] {a b : α}
-
-lemma abs_le_iff  : abs a ≤ b ↔ (- b ≤ a ∧ a ≤ b) :=
-⟨assume h, ⟨neg_le_of_neg_le $ le_trans (neg_le_abs_self _) h, le_trans (le_abs_self _) h⟩,
-  assume ⟨h₁, h₂⟩, abs_le_of_le_of_neg_le h₂ $ neg_le_of_neg_le h₁⟩
+section add_comm_group
+  variables [add_comm_group α] {a b c : α}
 
-lemma abs_lt_iff  : abs a < b ↔ (- b < a ∧ a < b) :=
-⟨assume h, ⟨neg_lt_of_neg_lt $ lt_of_le_of_lt (neg_le_abs_self _) h, lt_of_le_of_lt (le_abs_self _) h⟩,
-  assume ⟨h₁, h₂⟩, abs_lt_of_lt_of_neg_lt h₂ $ neg_lt_of_neg_lt h₁⟩
+  lemma sub_eq_neg_add (a b : α) : a - b = -b + a :=
+  by simp
 
-@[simp] lemma abs_eq_zero_iff : abs a = 0 ↔ a = 0 :=
-⟨eq_zero_of_abs_eq_zero, by simp [abs_zero] {contextual := tt}⟩
-
-end decidable_linear_ordered_comm_group
-
-/-
-namespace norm_num
-reveal add.assoc
+  theorem neg_add' (a b : α) : -(a + b) = -a - b := neg_add a b
 
-def add1 [has_add A] [has_one A] (a : A) : A := add a one
+  lemma eq_sub_iff_add_eq' : a = b - c ↔ c + a = b :=
+  by rw [eq_sub_iff_add_eq, add_comm]
 
-local attribute add1 bit0 bit1 [reducible]
+  lemma sub_eq_iff_eq_add' : a - b = c ↔ a = b + c :=
+  by rw [sub_eq_iff_eq_add, add_comm]
 
-theorem add_comm_four [add_comm_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) :=
-sorry -- by simp
+  lemma add_sub_cancel' (a b : α) : a + b - a = b :=
+  by simp
 
-theorem add_comm_middle [add_comm_semigroup A] (a b c : A) : a + b + c = a + c + b :=
-sorry -- by simp
+  lemma add_sub_cancel'_right (a b : α) : a + (b - a) = b :=
+  by rw [← add_sub_assoc, add_sub_cancel']
 
-theorem bit0_add_bit0 [add_comm_semigroup A] (a b : A) : bit0 a + bit0 b = bit0 (a + b) :=
-sorry -- by simp
+  lemma sub_sub_swap (a b c : α) : a - b - c = a - c - b :=
+  by simp
 
-theorem bit0_add_bit0_helper [add_comm_semigroup A] (a b t : A) (H : a + b = t) :
-        bit0 a + bit0 b = bit0 t :=
-sorry -- by rewrite -H; simp
+  lemma sub_sub_sub_cancel_left (a b c : α) : (c - a) - (c - b) = b - a :=
+  by simp
 
-theorem bit1_add_bit0 [add_comm_semigroup A] [has_one A] (a b : A) :
-        bit1 a + bit0 b = bit1 (a + b) :=
-sorry -- by simp
+end add_comm_group
 
-theorem bit1_add_bit0_helper [add_comm_semigroup A] [has_one A] (a b t : A)
-        (H : a + b = t) : bit1 a + bit0 b = bit1 t :=
-sorry -- by rewrite -H; simp
-
-theorem bit0_add_bit1 [add_comm_semigroup A] [has_one A] (a b : A) :
-        bit0 a + bit1 b = bit1 (a + b) :=
-sorry -- by simp
-
-theorem bit0_add_bit1_helper [add_comm_semigroup A] [has_one A] (a b t : A)
-        (H : a + b = t) : bit0 a + bit1 b = bit1 t :=
-sorry -- by rewrite -H; simp
-
-theorem bit1_add_bit1 [add_comm_semigroup A] [has_one A] (a b : A) :
-        bit1 a + bit1 b = bit0 (add1 (a + b)) :=
-sorry -- by simp
-
-theorem bit1_add_bit1_helper [add_comm_semigroup A] [has_one A] (a b t s: A)
-        (H : (a + b) = t) (H2 : add1 t = s) : bit1 a + bit1 b = bit0 s :=
-sorry -- by inst_simp
-
-theorem bin_add_zero [add_monoid A] (a : A) : a + zero = a :=
-sorry -- by simp
-
-theorem bin_zero_add [add_monoid A] (a : A) : zero + a = a :=
-sorry -- by simp
-
-theorem one_add_bit0 [add_comm_semigroup A] [has_one A] (a : A) : one + bit0 a = bit1 a :=
-sorry -- by simp
-
-theorem bit0_add_one [has_add A] [has_one A] (a : A) : bit0 a + one = bit1 a := rfl
-
-theorem bit1_add_one [has_add A] [has_one A] (a : A) : bit1 a + one = add1 (bit1 a) := rfl
-
-theorem bit1_add_one_helper [has_add A] [has_one A] (a t : A) (H : add1 (bit1 a) = t) :
-        bit1 a + one = t :=
-sorry -- by inst_simp
-
-theorem one_add_bit1 [add_comm_semigroup A] [has_one A] (a : A) : one + bit1 a = add1 (bit1 a) :=
-sorry -- by simp
-
-theorem one_add_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A)
-        (H : add1 (bit1 a) = t) : one + bit1 a = t :=
-sorry -- by inst_simp
-
-theorem add1_bit0 [has_add A] [has_one A] (a : A) : add1 (bit0 a) = bit1 a := rfl
-
-theorem add1_bit1 [add_comm_semigroup A] [has_one A] (a : A) :
-        add1 (bit1 a) = bit0 (add1 a) :=
-sorry -- by simp
-
-theorem add1_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A) (H : add1 a = t) :
-        add1 (bit1 a) = bit0 t :=
-sorry -- by inst_simp
-
-theorem add1_one [has_add A] [has_one A] : add1 (one : A) = bit0 one := rfl
-
-theorem add1_zero [add_monoid A] [has_one A] : add1 (zero : A) = one :=
-sorry -- by simp
-
-theorem one_add_one [has_add A] [has_one A] : (one : A) + one = bit0 one := rfl
-
-theorem subst_into_sum [has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
-        (prt : tl + tr = t) : l + r = t :=
-sorry -- by simp
-
-theorem neg_zero_helper [add_group A] (a : A) (H : a = 0) : - a = 0 :=
-sorry -- by simp
-
-end norm_num
+section ordered_comm_group
+variables [ordered_comm_group α]
 
-attribute [simp]
-  zero_add add_zero one_mul mul_one
+theorem le_sub_iff_add_le {a b c : α} : a ≤ b - c ↔ a + c ≤ b :=
+by rw [add_comm]; exact ⟨add_le_of_le_sub_left, le_sub_left_of_add_le⟩
 
-attribute [simp]
-  neg_neg sub_eq_add_neg
+theorem sub_le_iff_le_add {a b c : α} : a - c ≤ b ↔ a ≤ b + c :=
+by rw [add_comm]; exact ⟨le_add_of_sub_left_le, sub_left_le_of_le_add⟩
 
-attribute [simp]
-  add.assoc add.comm add.left_comm
-  mul.left_comm mul.comm mul.assoc
--/
+end ordered_comm_group
diff --git a/algebra/order.lean b/algebra/order.lean
new file mode 100644
index 0000000000000..b65eda31c0cf7
--- /dev/null
+++ b/algebra/order.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+
+universe u
+variables {α : Type u}
+
+lemma not_le_of_lt [preorder α] {a b : α} (h : a < b) : ¬ b ≤ a :=
+(le_not_le_of_lt h).right
+
+lemma not_lt_of_le [preorder α] {a b : α} (h : a ≤ b) : ¬ b < a
+| hab := not_le_of_gt hab h
+ 
+lemma not_lt_of_lt [linear_order α] {a b : α} (h : a < b) : ¬ b < a :=
+lt_asymm h
+
+lemma le_iff_eq_or_lt [partial_order α] {a b : α} : a ≤ b ↔ a = b ∨ a < b :=
+le_iff_lt_or_eq.trans or.comm
+
+@[simp] lemma not_lt [linear_order α] {a b : α} : ¬ a < b ↔ b ≤ a :=
+⟨(lt_or_ge a b).resolve_left, not_lt_of_le⟩
+
+lemma le_of_not_lt [linear_order α] {a b : α} : ¬ a < b → b ≤ a :=
+not_lt.1
+
+@[simp] lemma not_le [linear_order α] {a b : α} : ¬ a ≤ b ↔ b < a :=
+(lt_iff_le_not_le.trans ⟨and.right,
+  λ h, ⟨(le_total _ _).resolve_left h, h⟩⟩).symm
+
+lemma not_lt_iff_eq_or_lt [linear_order α] {a b : α} : ¬ a < b ↔ a = b ∨ b < a :=
+not_lt.trans $ le_iff_eq_or_lt.trans $ or_congr eq_comm iff.rfl
+
+lemma le_imp_le_iff_lt_imp_lt [linear_order α] {a b c d : α} :
+  (a ≤ b → c ≤ d) ↔ (d < c → b < a) :=
+⟨λ H h, lt_of_not_ge $ λ h', not_lt_of_ge (H h') h,
+λ H h, le_of_not_gt $ λ h', not_le_of_gt (H h') h⟩
+
+lemma le_iff_le_iff_lt_iff_lt [linear_order α] {a b c d : α} :
+  (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
+⟨λ H, not_le.symm.trans $ iff.trans (not_congr H) $ not_le,
+λ H, not_lt.symm.trans $ iff.trans (not_congr H) $ not_lt⟩
+
+lemma eq_of_forall_le_iff [partial_order α] {a b : α}
+  (H : ∀ c, c ≤ a ↔ c ≤ b) : a = b :=
+le_antisymm ((H _).1 (le_refl _)) ((H _).2 (le_refl _))
+
+lemma eq_of_forall_ge_iff [partial_order α] {a b : α}
+  (H : ∀ c, a ≤ c ↔ b ≤ c) : a = b :=
+le_antisymm ((H _).2 (le_refl _)) ((H _).1 (le_refl _))
diff --git a/algebra/ordered_group.lean b/algebra/ordered_group.lean
new file mode 100644
index 0000000000000..139b014e46aae
--- /dev/null
+++ b/algebra/ordered_group.lean
@@ -0,0 +1,255 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import algebra.group tactic
+
+universe u
+variable {α : Type u}
+
+section ordered_cancel_comm_monoid
+variables [ordered_cancel_comm_monoid α] {a b c : α}
+
+@[simp] lemma add_le_add_iff_left (a : α) {b c : α} : a + b ≤ a + c ↔ b ≤ c :=
+⟨le_of_add_le_add_left, λ h, add_le_add_left h _⟩
+
+@[simp] lemma add_le_add_iff_right (c : α) : a + c ≤ b + c ↔ a ≤ b :=
+add_comm c a ▸ add_comm c b ▸ add_le_add_iff_left c
+
+@[simp] lemma add_lt_add_iff_left (a : α) {b c : α} : a + b < a + c ↔ b < c :=
+⟨lt_of_add_lt_add_left, λ h, add_lt_add_left h _⟩
+
+@[simp] lemma add_lt_add_iff_right (c : α) : a + c < b + c ↔ a < b :=
+add_comm c a ▸ add_comm c b ▸ add_lt_add_iff_left c
+
+@[simp] lemma le_add_iff_nonneg_right (a : α) {b : α} : a ≤ a + b ↔ 0 ≤ b :=
+have a + 0 ≤ a + b ↔ 0 ≤ b, from add_le_add_iff_left a,
+by rwa add_zero at this
+
+@[simp] lemma le_add_iff_nonneg_left (a : α) {b : α} : a ≤ b + a ↔ 0 ≤ b :=
+by rw [add_comm, le_add_iff_nonneg_right]
+
+@[simp] lemma lt_add_iff_pos_right (a : α) {b : α} : a < a + b ↔ 0 < b :=
+have a + 0 < a + b ↔ 0 < b, from add_lt_add_iff_left a,
+by rwa add_zero at this
+
+@[simp] lemma lt_add_iff_pos_left (a : α) {b : α} : a < b + a ↔ 0 < b :=
+by rw [add_comm, lt_add_iff_pos_right]
+
+lemma add_eq_zero_iff_eq_zero_of_nonneg
+  (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
+⟨λ hab : a + b = 0, 
+by split; apply le_antisymm; try {assumption};
+   rw ← hab; simp [ha, hb],
+λ ⟨ha', hb'⟩, by rw [ha', hb', add_zero]⟩
+
+end ordered_cancel_comm_monoid
+
+section ordered_comm_group
+variables [ordered_comm_group α] {a b c : α}
+
+@[simp] lemma neg_le_neg_iff : -a ≤ -b ↔ b ≤ a :=
+have a + b + -a ≤ a + b + -b ↔ -a ≤ -b, from add_le_add_iff_left _,
+by simp at this; simp [this]
+
+lemma neg_le : -a ≤ b ↔ -b ≤ a :=
+have -a ≤ -(-b) ↔ -b ≤ a, from neg_le_neg_iff,
+by rwa neg_neg at this
+
+lemma le_neg : a ≤ -b ↔ b ≤ -a :=
+have -(-a) ≤ -b ↔ b ≤ -a, from neg_le_neg_iff,
+by rwa neg_neg at this
+
+@[simp] lemma neg_nonpos : -a ≤ 0 ↔ 0 ≤ a :=
+have -a ≤ -0 ↔ 0 ≤ a, from neg_le_neg_iff,
+by rwa neg_zero at this
+
+@[simp] lemma neg_nonneg : 0 ≤ -a ↔ a ≤ 0 :=
+have -0 ≤ -a ↔ a ≤ 0, from neg_le_neg_iff,
+by rwa neg_zero at this
+
+@[simp] lemma neg_lt_neg_iff : -a < -b ↔ b < a :=
+have a + b + -a < a + b + -b ↔ -a < -b, from add_lt_add_iff_left _,
+by simp at this; simp [this]
+
+lemma neg_lt_zero : -a < 0 ↔ 0 < a :=
+have -a < -0 ↔ 0 < a, from neg_lt_neg_iff,
+by rwa neg_zero at this
+
+lemma neg_pos : 0 < -a ↔ a < 0 :=
+have -0 < -a ↔ a < 0, from neg_lt_neg_iff,
+by rwa neg_zero at this
+
+lemma neg_lt : -a < b ↔ -b < a :=
+have -a < -(-b) ↔ -b < a, from neg_lt_neg_iff,
+by rwa neg_neg at this
+
+lemma lt_neg : a < -b ↔ b < -a :=
+have -(-a) < -b ↔ b < -a, from neg_lt_neg_iff,
+by rwa neg_neg at this
+
+lemma sub_le_sub_iff_left (a : α) {b c : α} : a - b ≤ a - c ↔ c ≤ b :=
+(add_le_add_iff_left _).trans neg_le_neg_iff
+
+lemma sub_le_sub_iff_right (c : α) : a - c ≤ b - c ↔ a ≤ b :=
+add_le_add_iff_right _
+
+lemma sub_lt_sub_iff_left (a : α) {b c : α} : a - b < a - c ↔ c < b :=
+(add_lt_add_iff_left _).trans neg_lt_neg_iff
+
+lemma sub_lt_sub_iff_right (c : α) : a - c < b - c ↔ a < b :=
+add_lt_add_iff_right _
+
+@[simp] lemma sub_nonneg : 0 ≤ a - b ↔ b ≤ a :=
+have a - a ≤ a - b ↔ b ≤ a, from sub_le_sub_iff_left a,
+by rwa sub_self at this
+
+@[simp] lemma sub_nonpos : a - b ≤ 0 ↔ a ≤ b :=
+have a - b ≤ b - b ↔ a ≤ b, from sub_le_sub_iff_right b,
+by rwa sub_self at this
+
+@[simp] lemma sub_pos : 0 < a - b ↔ b < a :=
+have a - a < a - b ↔ b < a, from sub_lt_sub_iff_left a,
+by rwa sub_self at this
+
+@[simp] lemma sub_lt_zero : a - b < 0 ↔ a < b :=
+have a - b < b - b ↔ a < b, from sub_lt_sub_iff_right b,
+by rwa sub_self at this
+
+@[simp] lemma le_neg_add_iff_add_le : b ≤ -a + c ↔ a + b ≤ c :=
+have -a + (a + b) ≤ -a + c ↔ a + b ≤ c, from add_le_add_iff_left _,
+by rwa neg_add_cancel_left at this
+
+lemma le_sub_left_iff_add_le : b ≤ c - a ↔ a + b ≤ c :=
+by rw [sub_eq_add_neg, add_comm, le_neg_add_iff_add_le]
+
+@[simp] lemma le_sub_right_iff_add_le : a ≤ c - b ↔ a + b ≤ c :=
+by rw [le_sub_left_iff_add_le, add_comm]
+
+@[simp] lemma neg_add_le_iff_le_add : -b + a ≤ c ↔ a ≤ b + c :=
+have -b + a ≤ -b + (b + c) ↔ a ≤ b + c, from add_le_add_iff_left _,
+by rwa neg_add_cancel_left at this
+
+lemma sub_left_le_iff_le_add : a - b ≤ c ↔ a ≤ b + c :=
+by rw [sub_eq_add_neg, add_comm, neg_add_le_iff_le_add]
+
+@[simp] lemma sub_right_le_iff_le_add : a - c ≤ b ↔ a ≤ b + c :=
+by rw [sub_left_le_iff_le_add, add_comm]
+
+lemma neg_add_le_iff_le_add_right : -c + a ≤ b ↔ a ≤ b + c :=
+by rw [neg_add_le_iff_le_add, add_comm]
+
+@[simp] lemma neg_le_sub_iff_le_add : -b ≤ a - c ↔ c ≤ a + b :=
+le_sub_right_iff_add_le.trans neg_add_le_iff_le_add_right
+
+lemma neg_le_sub_iff_le_add_left : -a ≤ b - c ↔ c ≤ a + b :=
+by rw [neg_le_sub_iff_le_add, add_comm]
+
+lemma sub_le : a - b ≤ c ↔ a - c ≤ b :=
+sub_left_le_iff_le_add.trans sub_right_le_iff_le_add.symm
+
+@[simp] lemma lt_neg_add_iff_add_lt : b < -a + c ↔ a + b < c :=
+have -a + (a + b) < -a + c ↔ a + b < c, from add_lt_add_iff_left _,
+by rwa neg_add_cancel_left at this
+
+lemma lt_sub_left_iff_add_lt : b < c - a ↔ a + b < c :=
+by rw [sub_eq_add_neg, add_comm, lt_neg_add_iff_add_lt]
+
+@[simp] lemma lt_sub_right_iff_add_lt : a < c - b ↔ a + b < c :=
+by rw [lt_sub_left_iff_add_lt, add_comm]
+
+@[simp] lemma neg_add_lt_iff_lt_add : -b + a < c ↔ a < b + c :=
+have -b + a < -b + (b + c) ↔ a < b + c, from add_lt_add_iff_left _,
+by rwa neg_add_cancel_left at this
+
+lemma sub_left_lt_iff_lt_add : a - b < c ↔ a < b + c :=
+by rw [sub_eq_add_neg, add_comm, neg_add_lt_iff_lt_add]
+
+@[simp] lemma sub_right_lt_iff_lt_add : a - c < b ↔ a < b + c :=
+by rw [sub_left_lt_iff_lt_add, add_comm]
+
+lemma neg_add_lt_iff_lt_add_right : -c + a < b ↔ a < b + c :=
+by rw [neg_add_lt_iff_lt_add, add_comm]
+
+@[simp] lemma neg_lt_sub_iff_lt_add : -b < a - c ↔ c < a + b :=
+lt_sub_right_iff_add_lt.trans neg_add_lt_iff_lt_add_right
+
+lemma neg_lt_sub_iff_lt_add_left : -a < b - c ↔ c < a + b :=
+by rw [neg_lt_sub_iff_lt_add, add_comm]
+
+lemma sub_lt : a - b < c ↔ a - c < b :=
+sub_left_lt_iff_lt_add.trans sub_right_lt_iff_lt_add.symm
+
+lemma sub_le_self_iff (a : α) {b : α} : a - b ≤ a ↔ 0 ≤ b :=
+sub_left_le_iff_le_add.trans (le_add_iff_nonneg_left _)
+
+lemma sub_lt_self_iff (a : α) {b : α} : a - b < a ↔ 0 < b :=
+sub_left_lt_iff_lt_add.trans (lt_add_iff_pos_left _)
+
+end ordered_comm_group
+
+-- This is not so much a new structure as a construction mechanism
+-- for ordered groups
+set_option old_structure_cmd true
+class nonneg_comm_group (α : Type*) extends add_comm_group α :=
+(nonneg : α → Prop)
+(pos : α → Prop := λ a, nonneg a ∧ ¬ nonneg (neg a))
+(pos_iff : ∀ a, pos a ↔ nonneg a ∧ ¬ nonneg (-a) . order_laws_tac)
+(zero_nonneg : nonneg 0)
+(add_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a + b))
+(nonneg_antisymm : ∀ {a}, nonneg a → nonneg (-a) → a = 0)
+
+namespace nonneg_comm_group
+variable [s : nonneg_comm_group α]
+include s
+
+@[reducible] instance to_ordered_comm_group : ordered_comm_group α :=
+{ s with
+  le := λ a b, nonneg (b - a),
+  lt := λ a b, pos (b - a),
+  lt_iff_le_not_le := λ a b, by simp; rw [pos_iff]; simp,
+  le_refl := λ a, by simp [zero_nonneg],
+  le_trans := λ a b c nab nbc, by simp [-sub_eq_add_neg];
+    rw ← sub_add_sub_cancel; exact add_nonneg nbc nab,
+  le_antisymm := λ a b nab nba, eq_of_sub_eq_zero $
+    nonneg_antisymm nba (by rw neg_sub; exact nab),
+  add_le_add_left := λ a b nab c, by simpf [(≤), preorder.le] at nab,
+  add_lt_add_left := λ a b nab c, by simpf [(<), preorder.lt] at nab }
+
+theorem nonneg_def {a : α} : nonneg a ↔ 0 ≤ a :=
+show _ ↔ nonneg _, by simp
+
+theorem pos_def {a : α} : pos a ↔ 0 < a :=
+show _ ↔ pos _, by simp
+
+theorem not_zero_pos : ¬ pos (0 : α) :=
+mt pos_def.1 (lt_irrefl _)
+
+theorem zero_lt_iff_nonneg_nonneg {a : α} :
+  0 < a ↔ nonneg a ∧ ¬ nonneg (-a) :=
+pos_def.symm.trans (pos_iff α _)
+
+theorem nonneg_total_iff :
+  (∀ a : α, nonneg a ∨ nonneg (-a)) ↔
+  (∀ a b : α, a ≤ b ∨ b ≤ a) :=
+⟨λ h a b, by have := h (b - a); rwa [neg_sub] at this,
+ λ h a, by rw [nonneg_def, nonneg_def, neg_nonneg]; apply h⟩
+
+def to_decidable_linear_ordered_comm_group
+  [decidable_pred (@nonneg α _)]
+  (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
+  : decidable_linear_ordered_comm_group α :=
+{ @nonneg_comm_group.to_ordered_comm_group _ s with
+  le := (≤),
+  lt := (<),
+  lt_iff_le_not_le := @lt_iff_le_not_le _ _,
+  le_refl := @le_refl _ _,
+  le_trans := @le_trans _ _,
+  le_antisymm := @le_antisymm _ _,
+  le_total := nonneg_total_iff.1 nonneg_total,
+  decidable_le := by apply_instance,
+  decidable_eq := by apply_instance,
+  decidable_lt := by apply_instance }
+
+end nonneg_comm_group
diff --git a/algebra/ordered_ring.lean b/algebra/ordered_ring.lean
new file mode 100644
index 0000000000000..a18aed43fef91
--- /dev/null
+++ b/algebra/ordered_ring.lean
@@ -0,0 +1,208 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import algebra.order algebra.ordered_group algebra.ring
+
+universe u
+variable {α : Type u}
+
+section linear_ordered_semiring
+variable [linear_ordered_semiring α]
+
+@[simp] lemma mul_le_mul_left {a b c : α} (h : 0 < c) : c * a ≤ c * b ↔ a ≤ b :=
+⟨λ h', le_of_mul_le_mul_left h' h, λ h', mul_le_mul_of_nonneg_left h' (le_of_lt h)⟩
+
+@[simp] lemma mul_le_mul_right {a b c : α} (h : 0 < c) : a * c ≤ b * c ↔ a ≤ b :=
+⟨λ h', le_of_mul_le_mul_right h' h, λ h', mul_le_mul_of_nonneg_right h' (le_of_lt h)⟩
+
+@[simp] lemma mul_lt_mul_left {a b c : α} (h : 0 < c) : c * a < c * b ↔ a < b :=
+⟨λ h', lt_of_mul_lt_mul_left h' (le_of_lt h), λ h', mul_lt_mul_of_pos_left h' h⟩
+
+@[simp] lemma mul_lt_mul_right {a b c : α} (h : 0 < c) : a * c < b * c ↔ a < b :=
+⟨λ h', lt_of_mul_lt_mul_right h' (le_of_lt h), λ h', mul_lt_mul_of_pos_right h' h⟩
+
+lemma le_mul_iff_one_le_left {a b : α} (hb : b > 0) : b ≤ a * b ↔ 1 ≤ a :=
+suffices 1 * b ≤ a * b ↔ 1 ≤ a, by rwa one_mul at this,
+mul_le_mul_right hb
+
+lemma lt_mul_iff_one_lt_left {a b : α} (hb : b > 0) : b < a * b ↔ 1 < a :=
+suffices 1 * b < a * b ↔ 1 < a, by rwa one_mul at this,
+mul_lt_mul_right hb
+
+lemma le_mul_iff_one_le_right {a b : α} (hb : b > 0) : b ≤ b * a ↔ 1 ≤ a :=
+suffices b * 1 ≤ b * a ↔ 1 ≤ a, by rwa mul_one at this,
+mul_le_mul_left hb
+
+lemma lt_mul_iff_one_lt_right {a b : α} (hb : b > 0) : b < b * a ↔ 1 < a :=
+suffices b * 1 < b * a ↔ 1 < a, by rwa mul_one at this,
+mul_lt_mul_left hb
+
+lemma lt_mul_of_gt_one_right' {a b : α} (hb : b > 0) : a > 1 → b < b * a :=
+(lt_mul_iff_one_lt_right hb).2
+
+lemma le_mul_of_ge_one_right' {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ b * a :=
+suffices b * 1 ≤ b * a, by rwa mul_one at this,
+mul_le_mul_of_nonneg_left h hb
+
+lemma le_mul_of_ge_one_left' {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ a * b :=
+suffices 1 * b ≤ a * b, by rwa one_mul at this,
+mul_le_mul_of_nonneg_right h hb
+
+end linear_ordered_semiring
+
+lemma linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero [s : linear_ordered_ring α]
+        {a b : α} (h : a * b = 0) : a = 0 ∨ b = 0 :=
+match lt_trichotomy 0 a with
+| or.inl hlt₁          :=
+  match lt_trichotomy 0 b with
+  | or.inl hlt₂          :=
+    have 0 < a * b, from mul_pos hlt₁ hlt₂,
+    begin rw h at this, exact absurd this (lt_irrefl _) end
+  | or.inr (or.inl heq₂) := or.inr heq₂.symm
+  | or.inr (or.inr hgt₂) :=
+    have 0 > a * b, from mul_neg_of_pos_of_neg hlt₁ hgt₂,
+    begin rw h at this, exact absurd this (lt_irrefl _)  end
+  end
+| or.inr (or.inl heq₁) := or.inl heq₁.symm
+| or.inr (or.inr hgt₁) :=
+  match lt_trichotomy 0 b with
+  | or.inl hlt₂          :=
+    have 0 > a * b, from mul_neg_of_neg_of_pos hgt₁ hlt₂,
+    begin rw h at this, exact absurd this (lt_irrefl _)  end
+  | or.inr (or.inl heq₂) := or.inr heq₂.symm
+  | or.inr (or.inr hgt₂) :=
+    have 0 < a * b, from mul_pos_of_neg_of_neg hgt₁ hgt₂,
+    begin rw h at this, exact absurd this (lt_irrefl _)  end
+  end
+end
+
+instance to_domain [s : linear_ordered_ring α] : domain α :=
+{ s with
+  eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α s }
+
+section linear_ordered_ring
+variable [linear_ordered_ring α]
+
+@[simp] lemma mul_le_mul_left_of_neg {a b c : α} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a :=
+⟨le_imp_le_iff_lt_imp_lt.2 $ λ h', mul_lt_mul_of_neg_left h' h,
+  λ h', mul_le_mul_of_nonpos_left h' (le_of_lt h)⟩
+
+@[simp] lemma mul_le_mul_right_of_neg {a b c : α} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a :=
+⟨le_imp_le_iff_lt_imp_lt.2 $ λ h', mul_lt_mul_of_neg_right h' h,
+  λ h', mul_le_mul_of_nonpos_right h' (le_of_lt h)⟩
+
+@[simp] lemma mul_lt_mul_left_of_neg {a b c : α} (h : c < 0) : c * a < c * b ↔ b < a :=
+le_iff_le_iff_lt_iff_lt.1 (mul_le_mul_left_of_neg h)
+
+@[simp] lemma mul_lt_mul_right_of_neg {a b c : α} (h : c < 0) : a * c < b * c ↔ b < a :=
+le_iff_le_iff_lt_iff_lt.1 (mul_le_mul_right_of_neg h)
+
+end linear_ordered_ring
+
+set_option old_structure_cmd true
+class nonneg_ring (α : Type*)
+  extends ring α, zero_ne_one_class α, nonneg_comm_group α :=
+(mul_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a * b))
+(mul_pos : ∀ {a b}, pos a → pos b → pos (a * b))
+
+class linear_nonneg_ring (α : Type*) extends domain α, nonneg_comm_group α :=
+(mul_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a * b))
+(nonneg_total : ∀ a, nonneg a ∨ nonneg (-a))
+
+namespace nonneg_ring
+open nonneg_comm_group
+variable [s : nonneg_ring α]
+
+instance to_ordered_ring : ordered_ring α :=
+{ s with
+  le := (≤),
+  lt := (<),
+  lt_iff_le_not_le := @lt_iff_le_not_le _ _,
+  le_refl := @le_refl _ _,
+  le_trans := @le_trans _ _,
+  le_antisymm := @le_antisymm _ _,
+  add_lt_add_left := @add_lt_add_left _ _,
+  add_le_add_left := @add_le_add_left _ _,
+  mul_nonneg := λ a b, by simp [nonneg_def.symm]; exact mul_nonneg,
+  mul_pos := λ a b, by simp [pos_def.symm]; exact mul_pos }
+
+def nonneg_ring.to_linear_nonneg_ring
+  (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
+  : linear_nonneg_ring α :=
+{ s with
+  nonneg_total := nonneg_total,
+  eq_zero_or_eq_zero_of_mul_eq_zero :=
+    suffices ∀ {a} b : α, nonneg a → a * b = 0 → a = 0 ∨ b = 0,
+    from λ a b, (nonneg_total a).elim (this b)
+      (λ na, by simpf at this b na),
+    suffices ∀ {a b : α}, nonneg a → nonneg b → a * b = 0 → a = 0 ∨ b = 0,
+    from λ a b na, (nonneg_total b).elim (this na)
+      (λ nb, by simpf at this na nb),
+    λ a b na nb z, classical.by_cases
+      (λ nna : nonneg (-a), or.inl (nonneg_antisymm na nna))
+      (λ pa, classical.by_cases
+        (λ nnb : nonneg (-b), or.inr (nonneg_antisymm nb nnb))
+        (λ pb, absurd z $ ne_of_gt $ pos_def.1 $ mul_pos
+          ((pos_iff _ _).2 ⟨na, pa⟩)
+          ((pos_iff _ _).2 ⟨nb, pb⟩))) }
+
+end nonneg_ring
+
+namespace linear_nonneg_ring
+open nonneg_comm_group
+variable [s : linear_nonneg_ring α]
+
+instance to_nonneg_ring : nonneg_ring α :=
+{ s with
+  mul_pos := λ a b pa pb,
+  let ⟨a1, a2⟩ := (pos_iff α a).1 pa,
+      ⟨b1, b2⟩ := (pos_iff α b).1 pb in
+  have ab : nonneg (a * b), from mul_nonneg a1 b1,
+  (pos_iff α _).2 ⟨ab, λ hn,
+    have a * b = 0, from nonneg_antisymm ab hn,
+    (eq_zero_or_eq_zero_of_mul_eq_zero _ _ this).elim
+      (ne_of_gt (pos_def.1 pa))
+      (ne_of_gt (pos_def.1 pb))⟩ }
+
+instance to_linear_order : linear_order α :=
+{ s with
+  le := (≤),
+  lt := (<),
+  lt_iff_le_not_le := @lt_iff_le_not_le _ _,
+  le_refl := @le_refl _ _,
+  le_trans := @le_trans _ _,
+  le_antisymm := @le_antisymm _ _,
+  le_total := nonneg_total_iff.1 nonneg_total }
+
+instance to_linear_ordered_ring : linear_ordered_ring α :=
+{ s with
+  le := (≤),
+  lt := (<),
+  lt_iff_le_not_le := @lt_iff_le_not_le _ _,
+  le_refl := @le_refl _ _,
+  le_trans := @le_trans _ _,
+  le_antisymm := @le_antisymm _ _,
+  le_total := @le_total _ _,
+  add_lt_add_left := @add_lt_add_left _ _,
+  add_le_add_left := @add_le_add_left _ _,
+  mul_nonneg := by simp [nonneg_def.symm]; exact @mul_nonneg _ _,
+  mul_pos := by simp [pos_def.symm]; exact @nonneg_ring.mul_pos _ _,
+  zero_lt_one := lt_of_not_ge $ λ (h : nonneg (0 - 1)), begin
+    rw [zero_sub] at h,
+    have := mul_nonneg h h, simp at this,
+    exact zero_ne_one _ (nonneg_antisymm this h).symm
+  end }
+
+instance to_decidable_linear_ordered_comm_ring
+  [decidable_pred (@nonneg α _)]
+  [comm : @is_commutative α (*)]
+  : decidable_linear_ordered_comm_ring α :=
+{ @linear_nonneg_ring.to_linear_ordered_ring _ s with
+  decidable_le := by apply_instance,
+  decidable_eq := by apply_instance,
+  decidable_lt := by apply_instance,
+  mul_comm := is_commutative.comm (*) }
+
+end linear_nonneg_ring
diff --git a/algebra/ring.lean b/algebra/ring.lean
index 44503d0413757..ad9ef0153c7c3 100644
--- a/algebra/ring.lean
+++ b/algebra/ring.lean
@@ -3,37 +3,42 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn
 -/
-open eq
+import algebra.group
 
-universe variable uu
-variable {A : Type uu}
+universe u
+variable {α : Type u}
 
-/- ring -/
+section
+  variable [semiring α]
+
+  theorem mul_two (n : α) : n * 2 = n + n :=
+  (left_distrib n 1 1).trans (by simp)
+end
 
 section
-  variables [ring A] (a b c d e : A)
+  variables [ring α] (a b c d e : α)
 
   theorem mul_add_eq_mul_add_iff_sub_mul_add_eq : a * e + c = b * e + d ↔ (a - b) * e + c = d :=
   calc
     a * e + c = b * e + d ↔ a * e + c = d + b * e : by simp
       ... ↔ a * e + c - b * e = d : iff.intro (λ h, begin simp [h] end) (λ h,
                                                     begin simp [h.symm] end)
-      ... ↔ (a - b) * e + c = d   : begin simp [@sub_eq_add_neg A, @right_distrib A] end
+      ... ↔ (a - b) * e + c = d   : begin simp [@sub_eq_add_neg α, @right_distrib α] end
 
   theorem sub_mul_add_eq_of_mul_add_eq_mul_add : a * e + c = b * e + d → (a - b) * e + c = d :=
   assume h,
   calc
-    (a - b) * e + c = (a * e + c) - b * e : begin simp [@sub_eq_add_neg A, @right_distrib A] end
-                ... = d                   : begin rewrite h, simp [@add_sub_cancel A] end
+    (a - b) * e + c = (a * e + c) - b * e : begin simp [@sub_eq_add_neg α, @right_distrib α] end
+                ... = d                   : begin rewrite h, simp [@add_sub_cancel α] end
 
   theorem mul_neg_one_eq_neg : a * (-1) = -a :=
     have a + a * -1 = 0, from calc
       a + a * -1 = a * 1 + a * -1 : by simp
              ... = a * (1 + -1)   : eq.symm (left_distrib a 1 (-1))
              ... = 0              : by simp,
-    symm (neg_eq_of_add_eq_zero this)
+    (neg_eq_of_add_eq_zero this).symm
 
-  theorem ne_zero_and_ne_zero_of_mul_ne_zero {a b : A} (h : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
+  theorem ne_zero_and_ne_zero_of_mul_ne_zero {a b : α} (h : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
   begin
     split,
       intro ha, apply h, simp [ha],
@@ -41,19 +46,63 @@ section
   end
 end
 
+section comm_ring
+  variable [comm_ring α]
+
+  @[simp] lemma dvd_neg (a b : α) : (a ∣ -b) ↔ (a ∣ b) :=
+  ⟨dvd_of_dvd_neg, dvd_neg_of_dvd⟩
+
+  @[simp] lemma neg_dvd (a b : α) : (-a ∣ b) ↔ (a ∣ b) :=
+  ⟨dvd_of_neg_dvd, neg_dvd_of_dvd⟩
+end comm_ring
+
+set_option old_structure_cmd true
+class domain (α : Type u) extends ring α, no_zero_divisors α, zero_ne_one_class α
+
+section domain
+  variable [domain α]
+
+  theorem mul_eq_zero {a b : α} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
+  ⟨eq_zero_or_eq_zero_of_mul_eq_zero, λo,
+    or.elim o (λh, by rw h; apply zero_mul) (λh, by rw h; apply mul_zero)⟩
+
+  theorem mul_ne_zero' {a b : α} (h₁ : a ≠ 0) (h₂ : b ≠ 0) : a * b ≠ 0 :=
+  λ h, or.elim (eq_zero_or_eq_zero_of_mul_eq_zero h) h₁ h₂
+
+  theorem domain.mul_right_inj {a b c : α} (ha : a ≠ 0) : b * a = c * a ↔ b = c :=
+  by rw [← sub_eq_zero, ← mul_sub_right_distrib, mul_eq_zero];
+     simp [ha]; exact sub_eq_zero
+
+  theorem domain.mul_left_inj {a b c : α} (ha : a ≠ 0) : a * b = a * c ↔ b = c :=
+  by rw [← sub_eq_zero, ← mul_sub_left_distrib, mul_eq_zero];
+     simp [ha]; exact sub_eq_zero
+
+  theorem eq_zero_of_mul_eq_self_right' {a b : α} (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 :=
+  by apply (mul_eq_zero.1 _).resolve_right (sub_ne_zero.2 h₁);
+     rw [mul_sub_left_distrib, mul_one, sub_eq_zero, h₂]
+
+  theorem eq_zero_of_mul_eq_self_left' {a b : α} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 :=
+  by apply (mul_eq_zero.1 _).resolve_left (sub_ne_zero.2 h₁);
+     rw [mul_sub_right_distrib, one_mul, sub_eq_zero, h₂]
+
+  theorem mul_ne_zero_comm' {a b : α} (h : a * b ≠ 0) : b * a ≠ 0 :=
+  mul_ne_zero' (ne_zero_of_mul_ne_zero_left h) (ne_zero_of_mul_ne_zero_right h)
+
+end domain
+
 /- integral domains -/
 
 section
-  variables [s : integral_domain A] (a b c d e : A)
+  variables [s : integral_domain α] (a b c d e : α)
   include s
 
-  theorem eq_of_mul_eq_mul_right_of_ne_zero {a b c : A} (ha : a ≠ 0) (h : b * a = c * a) : b = c :=
+  theorem eq_of_mul_eq_mul_right_of_ne_zero {a b c : α} (ha : a ≠ 0) (h : b * a = c * a) : b = c :=
   have b * a - c * a = 0, by simp [h],
   have (b - c) * a = 0, by rewrite [mul_sub_right_distrib, this],
   have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right ha,
   eq_of_sub_eq_zero this
 
-  theorem eq_of_mul_eq_mul_left_of_ne_zero {a b c : A} (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
+  theorem eq_of_mul_eq_mul_left_of_ne_zero {a b c : α} (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
   have a * b - a * c = 0, by simp [h],
   have a * (b - c) = 0, by rewrite [mul_sub_left_distrib, this],
   have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_left ha,
@@ -62,7 +111,7 @@ section
 
   -- TODO: do we want the iff versions?
 
---  theorem dvd_of_mul_dvd_mul_left {a b c : A} (Ha : a ≠ 0) (Hdvd : (a * b ∣ a * c)) : (b ∣ c) :=
+--  theorem dvd_of_mul_dvd_mul_left {a b c : α} (Ha : a ≠ 0) (Hdvd : (a * b ∣ a * c)) : (b ∣ c) :=
 --  sorry
   /-
   dvd.elim Hdvd
@@ -72,7 +121,7 @@ section
       dvd.intro this)
   -/
 
---  theorem dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : (b * a ∣ c * a)) : (b ∣ c) :=
+--  theorem dvd_of_mul_dvd_mul_right {a b c : α} (Ha : a ≠ 0) (Hdvd : (b * a ∣ c * a)) : (b ∣ c) :=
 --  sorry
   /-
   dvd.elim Hdvd
@@ -83,100 +132,3 @@ section
       dvd.intro this)
   -/
 end
-
-/-
-namespace norm_num
-
-local attribute bit0 bit1 add1 [reducible]
-local attribute right_distrib left_distrib [simp]
-
-theorem mul_zero [mul_zero_class A] (a : A) : a * zero = zero :=
-sorry -- by simp
-
-theorem zero_mul [mul_zero_class A] (a : A) : zero * a = zero :=
-sorry -- by simp
-
-theorem mul_one [monoid A] (a : A) : a * one = a :=
-sorry -- by simp
-
-theorem mul_bit0 [distrib A] (a b : A) : a * (bit0 b) = bit0 (a * b) :=
-sorry -- by simp
-
-theorem mul_bit0_helper [distrib A] (a b t : A) (h : a * b = t) : a * (bit0 b) = bit0 t :=
-sorry -- by rewrite -H; simp
-
-theorem mul_bit1 [semiring A] (a b : A) : a * (bit1 b) = bit0 (a * b) + a :=
-sorry -- by simp
-
-theorem mul_bit1_helper [semiring A] (a b s t : A) (Hs : a * b = s) (Ht : bit0 s + a  = t) :
-        a * (bit1 b) = t :=
-sorry -- by simp
-
-theorem subst_into_prod [has_mul A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
-        (prt : tl * tr = t) :
-        l * r = t :=
-sorry -- by simp
-
-theorem mk_cong (op : A → A) (a b : A) (h : a = b) : op a = op b :=
-sorry -- by simp
-
-theorem neg_add_neg_eq_of_add_add_eq_zero [add_comm_group A] (a b c : A) (h : c + a + b = 0) :
-        -a + -b = c :=
-sorry
-/-
-begin
-  apply add_neg_eq_of_eq_add,
-  apply neg_eq_of_add_eq_zero,
-  simp
-end
--/
-
-theorem neg_add_neg_helper [add_comm_group A] (a b c : A) (h : a + b = c) : -a + -b = -c :=
-sorry -- begin apply iff.mp !neg_eq_neg_iff_eq, simp end
-
-theorem neg_add_pos_eq_of_eq_add [add_comm_group A] (a b c : A) (h : b = c + a) : -a + b = c :=
-sorry -- begin apply neg_add_eq_of_eq_add, simp end
-
-theorem neg_add_pos_helper1 [add_comm_group A] (a b c : A) (h : b + c = a) : -a + b = -c :=
-sorry -- begin apply neg_add_eq_of_eq_add, apply eq_add_neg_of_add_eq H end
-
-theorem neg_add_pos_helper2 [add_comm_group A] (a b c : A) (h : a + c = b) : -a + b = c :=
-sorry -- begin apply neg_add_eq_of_eq_add, rewrite H end
-
-theorem pos_add_neg_helper [add_comm_group A] (a b c : A) (h : b + a = c) : a + b = c :=
-sorry -- by simp
-
-theorem sub_eq_add_neg_helper [add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁)
-        (H₂ : t₂ = w₂) (h : w₁ + -w₂ = e) : t₁ - t₂ = e :=
-sorry -- by simp
-
-theorem pos_add_pos_helper [add_comm_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂)
-        (h : h₁ + h₂ = c) : a + b = c :=
-sorry -- by simp
-
-theorem subst_into_subtr [add_group A] (l r t : A) (prt : l + -r = t) : l - r = t :=
-sorry -- by simp
-
-theorem neg_neg_helper [add_group A] (a b : A) (h : a = -b) : -a = b :=
-sorry -- by simp
-
-theorem neg_mul_neg_helper [ring A] (a b c : A) (h : a * b = c) : (-a) * (-b) = c :=
-sorry -- by simp
-
-theorem neg_mul_pos_helper [ring A] (a b c : A) (h : a * b = c) : (-a) * b = -c :=
-sorry -- by simp
-
-theorem pos_mul_neg_helper [ring A] (a b c : A) (h : a * b = c) : a * (-b) = -c :=
-sorry -- by simp
-
-end norm_num
-
-attribute [simp]
-  zero_mul mul_zero
-
-attribute [simp]
-  neg_mul_eq_neg_mul_symm mul_neg_eq_neg_mul_symm
-
-attribute [simp]
-  left_distrib right_distrib
--/
diff --git a/topology/ennreal.lean b/topology/ennreal.lean
index 0d4a10cb66e4b..c8f50e5f4036c 100644
--- a/topology/ennreal.lean
+++ b/topology/ennreal.lean
@@ -307,7 +307,7 @@ instance : decidable_linear_order ennreal :=
   decidable_le := by apply_instance }
 
 @[simp] lemma not_infty_lt : ¬ ∞ < a :=
-assume ⟨h₁, h₂⟩, h₂ le_infty
+by simp
 
 @[simp] lemma of_real_lt_infty : of_real r < ∞ :=
 ⟨le_infty, assume h, ennreal.no_confusion $ infty_le_iff.mp h⟩
@@ -321,7 +321,7 @@ forall_ennreal.mpr $ ⟨this, by simp⟩
 
 @[simp] lemma of_real_lt_of_real_iff :
   0 ≤ r → 0 ≤ p → (of_real r < of_real p ↔ r < p) :=
-by simp [lt_iff_le_not_le] {contextual:=tt}
+by simp [lt_iff_le_not_le, -not_le] {contextual:=tt}
 
 lemma lt_iff_exists_of_real : ∀{a b}, a < b ↔ (∃p, 0 ≤ p ∧ a = of_real p ∧ of_real p < b) :=
 by simp [forall_ennreal] {contextual := tt}; exact assume r hr,
@@ -340,7 +340,7 @@ by_cases
   (by simp [lt_irrefl, not_imp_not, le_of_lt, of_real_of_not_nonneg] {contextual := tt})
 
 @[simp] lemma not_lt_zero : ¬ a < 0 :=
-assume h, lt_irrefl a $ lt_of_lt_of_le h ennreal.zero_le
+by simp
 
 protected lemma zero_lt_one : 0 < (1 : ennreal) :=
 zero_lt_of_real_iff.mpr zero_lt_one
diff --git a/topology/metric_space.lean b/topology/metric_space.lean
index 494fcc43cec52..46a1c6aebfcba 100644
--- a/topology/metric_space.lean
+++ b/topology/metric_space.lean
@@ -91,7 +91,7 @@ instance : metric_space ℝ :=
 { real.uniform_space with
   dist := λx y, abs (x - y),
   dist_self := by simp [abs_zero],
-  eq_of_dist_eq_zero := by simp [add_eq_iff_eq_add_neg] {contextual := tt},
+  eq_of_dist_eq_zero := by simp,
   dist_comm := assume x y, by rw [abs_sub],
   dist_triangle := assume x y z, abs_sub_le _ _ _,
   uniformity_dist := le_antisymm
diff --git a/topology/real.lean b/topology/real.lean
index accfbf839fa9d..b9241bc72e8bd 100644
--- a/topology/real.lean
+++ b/topology/real.lean
@@ -22,7 +22,8 @@ generalizations:
 
 -/
 
-import topology.uniform_space topology.topological_structures data.rat algebra.field
+import topology.uniform_space topology.topological_structures data.rat
+       algebra.field algebra.functions algebra.order algebra.ordered_group
 noncomputable theory
 open classical set lattice filter
 local attribute [instance] decidable_inhabited prop_decidable
@@ -80,7 +81,7 @@ begin
   { intros r hr,
     have h : {b | abs (a + -b) < r} = {b | a - r < b} ∩ {b | b < a + r},
       from (set.ext $ assume b,
-        by simp [abs_lt_iff, -sub_eq_add_neg, (sub_eq_add_neg _ _).symm, sub_lt_iff, lt_sub_iff]),
+        by simp [abs_lt, -sub_eq_add_neg, (sub_eq_add_neg _ _).symm, sub_lt, lt_sub_iff]),
     rw [h, ←inf_principal],
     apply le_inf _ _,
     exact (infi_le_of_le {b : α | a - r < b} $ infi_le_of_le (sub_lt_self a hr) $
@@ -409,7 +410,7 @@ have ∀{r:ℚ}, {q | abs q ≤ abs r + 1} ∈ (nhds r).sets,
   have r < 1 + abs r, from lt_of_le_of_lt (le_abs_self r) (lt_add_of_pos_left _ zero_lt_one),
   have {q : ℚ | q ≤ 1 + abs r} ∩ {q:ℚ | -1 + -abs r ≤ q} ∈ (nhds r).sets,
     from inter_mem_sets (ge_mem_nhds ‹r < 1 + abs r›) (le_mem_nhds ‹-1 + -abs r < r›),
-  by simp [abs_le_iff]; exact this,
+  by simpf [abs_le],
 have h : {a : ℚ × ℚ | abs (a.fst) ≤ abs r + 1 ∧ abs (a.snd) ≤ abs q + 1} ∈ (nhds (r, q)).sets,
   by rw [nhds_prod_eq]; exact prod_mem_prod this this,
 have uniform_continuous (λp:{p:ℚ×ℚ // abs p.1 ≤ abs r + 1 ∧ abs p.2 ≤ abs q + 1}, p.1.1 * p.1.2),
@@ -677,7 +678,7 @@ have ∀ r∈nonneg, f r ∈ closure ({0} : set ℝ),
       from assume a ⟨q, (hq : 0 ≤ q), hrq⟩,
       by simp [hrq.symm, of_rat_abs_real, abs_neg, abs_of_nonneg hq],
 have h₁ : ∀{r}, r ∈ nonneg → abs_real (- r) + (- r) = 0,
-  from assume r hr, show f r = 0, by simp [closure_singleton] at this; exact this _ hr,
+  from assume r hr, show f r = 0, by specialize this _ hr; simpf [closure_singleton],
 have h₂ : ∀r, r = d (r + r),
   from is_closed_property dense_embedding_of_rat.closure_image_univ
     (is_closed_eq continuous_id $ continuous_compose (continuous_add continuous_id continuous_id) c_d)
@@ -711,13 +712,12 @@ instance : linear_order ℝ :=
 { le := (≤),
   le_refl := assume a, show (a - a) ∈ nonneg, by simp; exact of_rat_mem_nonneg (le_refl _),
   le_trans := assume a b c (h₁ : b - a ∈ nonneg) (h₂ : c - b ∈ nonneg),
-    have (c - b) + (b - a) ∈ nonneg,
-      from mem_nonneg_of_continuous2 continuous_add' h₂ h₁ $
-        assume a b ha hb, by rw [of_rat_add]; exact of_rat_mem_nonneg (le_add_of_le_of_nonneg ha hb),
     have (c - b) + (b - a) = c - a,
       from calc (c - b) + (b - a) = c + - a + (b + -b) : by simp [-add_right_neg]
         ... = c - a : by simp [-of_rat_zero],
-    show (c - a) ∈ nonneg, by simp * at *,
+    show (c - a) ∈ nonneg, by rw ← this;
+      refine mem_nonneg_of_continuous2 continuous_add' h₂ h₁ (λ a b ha hb, _);
+      rw [of_rat_add]; exact of_rat_mem_nonneg (le_add_of_le_of_nonneg ha hb),
   le_antisymm := assume a b (h₁ : b - a ∈ nonneg)  (h₂ : a - b ∈ nonneg),
     have h₁ : - (a - b) ∈ nonneg, by simp at h₁; simp [*],
     eq_of_sub_eq_zero $ eq_0_of_nonneg_of_neg_nonneg h₂ h₁,
@@ -738,14 +738,11 @@ instance : linear_order ℝ :=
     show b - a ∈ nonneg ∨ a - b ∈ nonneg, by simp [*] at * }
 
 lemma of_rat_lt_of_rat {q₁ q₂ : ℚ} : of_rat q₁ < of_rat q₂ ↔ q₁ < q₂ :=
-by simp [lt_iff_le_not_le, of_rat_le_of_rat]
+by simp [lt_iff_le_not_le, -not_le, of_rat_le_of_rat]
 
 private lemma add_le_add_left_iff {a b c : ℝ} : (c + a ≤ c + b) ↔ a ≤ b :=
-have (c + b) - (c + a) = b - a,
-  from calc (c + b) - (c + a) = c + - c + (b - a) : by simp [-add_right_neg]
-    ... = b - a : by simp [-of_rat_zero],
 show (c + b) - (c + a) ∈ nonneg ↔ b - a ∈ nonneg,
-  from by rwa [this]
+  by rwa [add_sub_add_left_eq_sub]
 
 instance : decidable_linear_ordered_comm_group ℝ :=
 { real.add_comm_group with
@@ -758,7 +755,7 @@ instance : decidable_linear_ordered_comm_group ℝ :=
   lt_iff_le_not_le := assume a b, lt_iff_le_not_le,
   add_le_add_left := assume a b h c, by rwa [add_le_add_left_iff],
   add_lt_add_left :=
-    assume a b, by simp [lt_iff_not_ge, ge, -add_comm, add_le_add_left_iff] {contextual := tt},
+    assume a b, by simp [lt_iff_not_ge, ge, -not_le, -add_comm, add_le_add_left_iff] {contextual := tt},
   decidable_eq    := by apply_instance,
   decidable_le    := by apply_instance,
   decidable_lt    := by apply_instance }
@@ -947,7 +944,7 @@ have ∀r:ℝ, ∃(s:set ℚ) (q:ℚ),
   from assume r,
   let ⟨q, (hrq : abs r < of_rat q)⟩ := exists_lt_of_rat (abs r) in
   have hq : 0 < q, from of_rat_lt_of_rat.mp $ lt_of_le_of_lt (abs_nonneg _) hrq,
-  have h_eq : {r : ℝ | of_rat (-q) ≤ r ∧ r ≤ of_rat q} = {r:ℝ | abs r ≤ of_rat q}, by simp [abs_le_iff],
+  have h_eq : {r : ℝ | of_rat (-q) ≤ r ∧ r ≤ of_rat q} = {r:ℝ | abs r ≤ of_rat q}, by simp [abs_le],
   have {r:ℝ | abs r < of_rat q} ∈ (nhds r).sets,
     from mem_nhds_sets (is_open_lt continuous_abs_real continuous_const) hrq,
   ⟨{p:ℚ | - q ≤ p ∧ p ≤ q}, q, hq,
@@ -959,7 +956,7 @@ have ∀r:ℝ, ∃(s:set ℚ) (q:ℚ),
     is_closed_inter
       (is_closed_le continuous_const continuous_id)
       (is_closed_le continuous_id continuous_const),
-    assume x, abs_le_iff.mpr⟩,
+    assume x, abs_le.2⟩,
 begin
   rw [real.has_mul],
   simp [lift_rat_op],
@@ -1142,7 +1139,7 @@ instance : discrete_linear_ordered_field ℝ :=
   zero_lt_one     := of_rat_lt_of_rat.mpr zero_lt_one,
   add_le_add_left := assume a b h c, by rwa [add_le_add_left_iff],
   add_lt_add_left :=
-    assume a b, by simp [lt_iff_not_ge, ge, -add_comm, add_le_add_left_iff] {contextual := tt},
+    assume a b, by simp [lt_iff_not_ge, ge, -not_le, -add_comm, add_le_add_left_iff] {contextual := tt},
   mul_nonneg      := assume a b, mul_nonneg,
   mul_pos         := assume a b ha hb,
     lt_of_le_of_ne (mul_nonneg (le_of_lt ha) (le_of_lt hb)) $