diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean
index 40f61ccdec24e..4ab806a6c4c30 100644
--- a/src/algebra/ordered_group.lean
+++ b/src/algebra/ordered_group.lean
@@ -61,14 +61,8 @@ with a partial order in which multiplication is strictly monotone. -/
 @[protect_proj, ancestor comm_group partial_order]
 class ordered_comm_group (α : Type u) extends comm_group α, partial_order α :=
 (mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
-
 attribute [to_additive] ordered_comm_group
 
-@[to_additive]
-instance units.covariant_class [ordered_comm_monoid α] :
-  covariant_class (units α) (units α) (*) (≤) :=
-{ elim := λ a b c bc, show (a : α) * b ≤ a * c, from mul_le_mul_left' bc _ }
-
 @[to_additive]
 instance ordered_comm_group.to_covariant_class_left_le (α : Type u) [ordered_comm_group α] :
   covariant_class α α (*) (≤) :=
@@ -81,9 +75,6 @@ instance units.ordered_comm_group [ordered_comm_monoid α] : ordered_comm_group
   .. units.partial_order,
   .. (infer_instance : comm_group (units α)) }
 
-section ordered_comm_group
-variables [ordered_comm_group α] {a b c d : α}
-
 @[priority 100, to_additive]    -- see Note [lower instance priority]
 instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u)
   [s : ordered_comm_group α] :
@@ -98,341 +89,433 @@ instance ordered_comm_group.has_exists_mul_of_le (α : Type u)
   has_exists_mul_of_le α :=
 ⟨λ a b hab, ⟨b * a⁻¹, (mul_inv_cancel_comm_assoc a b).symm⟩⟩
 
-@[to_additive neg_le_neg]
-lemma inv_le_inv' (h : a ≤ b) : b⁻¹ ≤ a⁻¹ :=
-have 1 ≤ a⁻¹ * b,           from mul_left_inv a ▸ mul_le_mul_left' h _,
-have 1 * b⁻¹ ≤ a⁻¹ * b * b⁻¹, from mul_le_mul_right' this _,
-by rwa [mul_inv_cancel_right, one_mul] at this
+section group
+variables [group α]
 
-@[to_additive]
-lemma le_of_inv_le_inv (h : b⁻¹ ≤ a⁻¹) : a ≤ b :=
-suffices (a⁻¹)⁻¹ ≤ (b⁻¹)⁻¹, from
-  begin simp [inv_inv] at this, assumption end,
-inv_le_inv' h
+section typeclasses_left_le
+variables [has_le α] [covariant_class α α (*) (≤)] {a b c d : α}
 
-@[to_additive]
-lemma one_le_of_inv_le_one (h : a⁻¹ ≤ 1) : 1 ≤ a :=
-have a⁻¹ ≤ 1⁻¹, by rwa one_inv,
-le_of_inv_le_inv this
+/--  Uses `left` co(ntra)variant. -/
+@[simp, to_additive left.neg_nonpos_iff]
+lemma left.inv_le_one_iff :
+  a⁻¹ ≤ 1 ↔ 1 ≤ a :=
+by { rw [← mul_le_mul_iff_left a], simp }
 
-@[to_additive]
-lemma inv_le_one_of_one_le (h : 1 ≤ a) : a⁻¹ ≤ 1 :=
-have a⁻¹ ≤ 1⁻¹, from inv_le_inv' h,
-by rwa one_inv at this
+/--  Uses `left` co(ntra)variant. -/
+@[simp, to_additive left.nonneg_neg_iff]
+lemma left.one_le_inv_iff :
+  1 ≤ a⁻¹ ↔ a ≤ 1 :=
+by { rw [← mul_le_mul_iff_left a], simp }
 
-@[to_additive nonpos_of_neg_nonneg]
-lemma le_one_of_one_le_inv (h : 1 ≤ a⁻¹) : a ≤ 1 :=
-have 1⁻¹ ≤ a⁻¹, by rwa one_inv,
-le_of_inv_le_inv this
+@[simp, to_additive]
+lemma le_inv_mul_iff_mul_le : b ≤ a⁻¹ * c ↔ a * b ≤ c :=
+by { rw ← mul_le_mul_iff_left a, simp }
 
-@[to_additive neg_nonneg_of_nonpos]
-lemma one_le_inv_of_le_one (h : a ≤ 1) : 1 ≤ a⁻¹ :=
-have 1⁻¹ ≤ a⁻¹, from inv_le_inv' h,
-by rwa one_inv at this
+@[simp, to_additive]
+lemma inv_mul_le_iff_le_mul : b⁻¹ * a ≤ c ↔ a ≤ b * c :=
+by rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]
 
-@[to_additive neg_lt_neg]
-lemma inv_lt_inv' (h : a < b) : b⁻¹ < a⁻¹ :=
-have 1 < a⁻¹ * b, from mul_left_inv a ▸ mul_lt_mul_left' h (a⁻¹),
-have 1 * b⁻¹ < a⁻¹ * b * b⁻¹, from mul_lt_mul_right' this (b⁻¹),
-by rwa [mul_inv_cancel_right, one_mul] at this
+@[to_additive neg_le_iff_add_nonneg']
+lemma inv_le_iff_one_le_mul' : a⁻¹ ≤ b ↔ 1 ≤ a * b :=
+(mul_le_mul_iff_left a).symm.trans $ by rw mul_inv_self
 
 @[to_additive]
-lemma lt_of_inv_lt_inv (h : b⁻¹ < a⁻¹) : a < b :=
-inv_inv a ▸ inv_inv b ▸ inv_lt_inv' h
+lemma le_inv_iff_mul_le_one_left : a ≤ b⁻¹ ↔ b * a ≤ 1 :=
+(mul_le_mul_iff_left b).symm.trans $ by rw mul_inv_self
 
 @[to_additive]
-lemma one_lt_of_inv_inv (h : a⁻¹ < 1) : 1 < a :=
-have a⁻¹ < 1⁻¹, by rwa one_inv,
-lt_of_inv_lt_inv this
+lemma le_inv_mul_iff_le : 1 ≤ b⁻¹ * a ↔ b ≤ a :=
+by rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]
 
 @[to_additive]
-lemma inv_inv_of_one_lt (h : 1 < a) : a⁻¹ < 1 :=
-have a⁻¹ < 1⁻¹, from inv_lt_inv' h,
-by rwa one_inv at this
+lemma inv_mul_le_one_iff : a⁻¹ * b ≤ 1 ↔ b ≤ a :=
+trans (inv_mul_le_iff_le_mul) $ by rw mul_one
 
-@[to_additive neg_of_neg_pos]
-lemma inv_of_one_lt_inv (h : 1 < a⁻¹) : a < 1 :=
-have 1⁻¹ < a⁻¹, by rwa one_inv,
-lt_of_inv_lt_inv this
+end typeclasses_left_le
 
-@[to_additive neg_pos_of_neg]
-lemma one_lt_inv_of_inv (h : a < 1) : 1 < a⁻¹ :=
-have 1⁻¹ < a⁻¹, from inv_lt_inv' h,
-by rwa one_inv at this
+section typeclasses_left_lt
+variables [has_lt α] [covariant_class α α (*) (<)] {a b c : α}
 
-@[to_additive]
-lemma le_inv_of_le_inv (h : a ≤ b⁻¹) : b ≤ a⁻¹ :=
-begin
-  have h := inv_le_inv' h,
-  rwa inv_inv at h
-end
+/--  Uses `left` co(ntra)variant. -/
+@[simp, to_additive left.neg_pos_iff]
+lemma left.one_lt_inv_iff :
+  1 < a⁻¹ ↔ a < 1 :=
+by rw [← mul_lt_mul_iff_left a, mul_inv_self, mul_one]
 
-@[to_additive]
-lemma inv_le_of_inv_le (h : a⁻¹ ≤ b) : b⁻¹ ≤ a :=
-begin
-  have h := inv_le_inv' h,
-  rwa inv_inv at h
-end
+/--  Uses `left` co(ntra)variant. -/
+@[simp, to_additive left.neg_neg_iff]
+lemma left.inv_lt_one_iff :
+  a⁻¹ < 1 ↔ 1 < a :=
+by rw [← mul_lt_mul_iff_left a, mul_inv_self, mul_one]
 
-@[to_additive]
-lemma lt_inv_of_lt_inv (h : a < b⁻¹) : b < a⁻¹ :=
-begin
-  have h := inv_lt_inv' h,
-  rwa inv_inv at h
-end
+@[simp, to_additive]
+lemma lt_inv_mul_iff_mul_lt : b < a⁻¹ * c ↔ a * b < c :=
+by { rw [← mul_lt_mul_iff_left a], simp }
 
-@[to_additive]
-lemma inv_lt_of_inv_lt (h : a⁻¹ < b) : b⁻¹ < a :=
-begin
-  have h := inv_lt_inv' h,
-  rwa inv_inv at h
-end
+@[simp, to_additive]
+lemma inv_mul_lt_iff_lt_mul : b⁻¹ * a < c ↔ a < b * c :=
+by rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]
 
 @[to_additive]
-lemma mul_le_of_le_inv_mul (h : b ≤ a⁻¹ * c) : a * b ≤ c :=
-begin
-  have h := mul_le_mul_left' h a,
-  rwa mul_inv_cancel_left at h
-end
+lemma inv_lt_iff_one_lt_mul' : a⁻¹ < b ↔ 1 < a * b :=
+(mul_lt_mul_iff_left a).symm.trans $ by rw mul_inv_self
 
 @[to_additive]
-lemma le_inv_mul_of_mul_le (h : a * b ≤ c) : b ≤ a⁻¹ * c :=
-begin
-  have h := mul_le_mul_left' h a⁻¹,
-  rwa inv_mul_cancel_left at h
-end
+lemma lt_inv_iff_mul_lt_one' : a < b⁻¹ ↔ b * a < 1 :=
+(mul_lt_mul_iff_left b).symm.trans $ by rw mul_inv_self
 
 @[to_additive]
-lemma le_mul_of_inv_mul_le (h : b⁻¹ * a ≤ c) : a ≤ b * c :=
-begin
-  have h := mul_le_mul_left' h b,
-  rwa mul_inv_cancel_left at h
-end
+lemma lt_inv_mul_iff_lt : 1 < b⁻¹ * a ↔ b < a :=
+by rw [← mul_lt_mul_iff_left b, mul_one, mul_inv_cancel_left]
 
 @[to_additive]
-lemma inv_mul_le_of_le_mul (h : a ≤ b * c) : b⁻¹ * a ≤ c :=
-begin
-  have h := mul_le_mul_left' h b⁻¹,
-  rwa inv_mul_cancel_left at h
-end
+lemma inv_mul_lt_one_iff : a⁻¹ * b < 1 ↔ b < a :=
+trans (inv_mul_lt_iff_lt_mul) $ by rw mul_one
 
-@[to_additive]
-lemma le_mul_of_inv_mul_le_left (h : b⁻¹ * a ≤ c) : a ≤ b * c :=
-le_mul_of_inv_mul_le h
+end typeclasses_left_lt
 
-@[to_additive]
-lemma inv_mul_le_left_of_le_mul (h : a ≤ b * c) : b⁻¹ * a ≤ c :=
-inv_mul_le_of_le_mul h
+section typeclasses_right_le
+variables [has_le α] [covariant_class α α (function.swap (*)) (≤)] {a b c : α}
 
-@[to_additive]
-lemma le_mul_of_inv_mul_le_right (h : c⁻¹ * a ≤ b) : a ≤ b * c :=
-by { rw mul_comm, exact le_mul_of_inv_mul_le h }
+/--  Uses `right` co(ntra)variant. -/
+@[simp, to_additive right.neg_nonpos_iff]
+lemma right.inv_le_one_iff :
+  a⁻¹ ≤ 1 ↔ 1 ≤ a :=
+by { rw [← mul_le_mul_iff_right a], simp }
 
-@[to_additive]
-lemma inv_mul_le_right_of_le_mul (h : a ≤ b * c) : c⁻¹ * a ≤ b :=
-by { rw mul_comm at h, apply inv_mul_le_left_of_le_mul h }
+/--  Uses `right` co(ntra)variant. -/
+@[simp, to_additive right.nonneg_neg_iff]
+lemma right.one_le_inv_iff :
+  1 ≤ a⁻¹ ↔ a ≤ 1 :=
+by { rw [← mul_le_mul_iff_right a], simp }
 
-@[to_additive]
-lemma mul_lt_of_lt_inv_mul (h : b < a⁻¹ * c) : a * b < c :=
-begin
-  have h := mul_lt_mul_left' h a,
-  rwa mul_inv_cancel_left at h
-end
+@[to_additive neg_le_iff_add_nonneg]
+lemma inv_le_iff_one_le_mul : a⁻¹ ≤ b ↔ 1 ≤ b * a :=
+(mul_le_mul_iff_right a).symm.trans $ by rw inv_mul_self
 
 @[to_additive]
-lemma lt_inv_mul_of_mul_lt (h : a * b < c) : b < a⁻¹ * c :=
-begin
-  have h := mul_lt_mul_left' h (a⁻¹),
-  rwa inv_mul_cancel_left at h
-end
+lemma le_inv_iff_mul_le_one_right : a ≤ b⁻¹ ↔ a * b ≤ 1 :=
+(mul_le_mul_iff_right b).symm.trans $ by rw inv_mul_self
+
+@[simp, to_additive]
+lemma mul_inv_le_iff_le_mul : a * b⁻¹ ≤ c ↔ a ≤ c * b :=
+(mul_le_mul_iff_right b).symm.trans $ by rw inv_mul_cancel_right
+
+@[simp, to_additive]
+lemma le_mul_inv_iff_mul_le : c ≤ a * b⁻¹ ↔ c * b ≤ a :=
+(mul_le_mul_iff_right b).symm.trans $ by rw inv_mul_cancel_right
+
+@[simp, to_additive]
+lemma mul_inv_le_one_iff_le : a * b⁻¹ ≤ 1 ↔ a ≤ b :=
+mul_inv_le_iff_le_mul.trans $ by rw one_mul
 
 @[to_additive]
-lemma lt_mul_of_inv_mul_lt (h : b⁻¹ * a < c) : a < b * c :=
-begin
-  have h := mul_lt_mul_left' h b,
-  rwa mul_inv_cancel_left at h
-end
+lemma le_mul_inv_iff_le : 1 ≤ a * b⁻¹ ↔ b ≤ a :=
+by rw [← mul_le_mul_iff_right b, one_mul, inv_mul_cancel_right]
 
 @[to_additive]
-lemma inv_mul_lt_of_lt_mul (h : a < b * c) : b⁻¹ * a < c :=
-begin
-  have h := mul_lt_mul_left' h (b⁻¹),
-  rwa inv_mul_cancel_left at h
-end
+lemma mul_inv_le_one_iff : b * a⁻¹ ≤ 1 ↔ b ≤ a :=
+trans (mul_inv_le_iff_le_mul) $ by rw one_mul
+
+end typeclasses_right_le
+
+section typeclasses_right_lt
+variables [has_lt α] [covariant_class α α (function.swap (*)) (<)] {a b c : α}
+
+/--  Uses `right` co(ntra)variant. -/
+@[simp, to_additive right.neg_neg_iff]
+lemma right.inv_lt_one_iff :
+  a⁻¹ < 1 ↔ 1 < a :=
+by rw [← mul_lt_mul_iff_right a, inv_mul_self, one_mul]
+
+/--  Uses `right` co(ntra)variant. -/
+@[simp, to_additive right.neg_pos_iff]
+lemma right.one_lt_inv_iff :
+  1 < a⁻¹ ↔ a < 1 :=
+by rw [← mul_lt_mul_iff_right a, inv_mul_self, one_mul]
 
 @[to_additive]
-lemma lt_mul_of_inv_mul_lt_left (h : b⁻¹ * a < c) : a < b * c :=
-lt_mul_of_inv_mul_lt h
+lemma inv_lt_iff_one_lt_mul : a⁻¹ < b ↔ 1 < b * a :=
+(mul_lt_mul_iff_right a).symm.trans $ by rw inv_mul_self
 
 @[to_additive]
-lemma inv_mul_lt_left_of_lt_mul (h : a < b * c) : b⁻¹ * a < c :=
-inv_mul_lt_of_lt_mul h
+lemma lt_inv_iff_mul_lt_one : a < b⁻¹ ↔ a * b < 1 :=
+(mul_lt_mul_iff_right b).symm.trans $ by rw inv_mul_self
+
+@[simp, to_additive]
+lemma mul_inv_lt_iff_lt_mul : a * b⁻¹ < c ↔ a < c * b :=
+by rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right]
+
+@[simp, to_additive]
+lemma lt_mul_inv_iff_mul_lt : c < a * b⁻¹ ↔ c * b < a :=
+(mul_lt_mul_iff_right b).symm.trans $ by rw inv_mul_cancel_right
+
+@[simp, to_additive]
+lemma inv_mul_lt_one_iff_lt : a * b⁻¹ < 1 ↔ a < b :=
+by rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right, one_mul]
 
 @[to_additive]
-lemma lt_mul_of_inv_mul_lt_right (h : c⁻¹ * a < b) : a < b * c :=
-by { rw mul_comm, exact lt_mul_of_inv_mul_lt h }
+lemma lt_mul_inv_iff_lt : 1 < a * b⁻¹ ↔ b < a :=
+by rw [← mul_lt_mul_iff_right b, one_mul, inv_mul_cancel_right]
 
 @[to_additive]
-lemma inv_mul_lt_right_of_lt_mul (h : a < b * c) : c⁻¹ * a < b :=
-by { rw mul_comm at h, exact inv_mul_lt_of_lt_mul h }
+lemma mul_inv_lt_one_iff : b * a⁻¹ < 1 ↔ b < a :=
+trans (mul_inv_lt_iff_lt_mul) $ by rw one_mul
 
-@[simp, to_additive]
-lemma inv_lt_one_iff_one_lt : a⁻¹ < 1 ↔ 1 < a :=
-⟨ one_lt_of_inv_inv, inv_inv_of_one_lt ⟩
+end typeclasses_right_lt
+
+section typeclasses_left_right_le
+variables [has_le α] [covariant_class α α (*) (≤)] [covariant_class α α (function.swap (*)) (≤)]
+  {a b c d : α}
 
 @[simp, to_additive]
 lemma inv_le_inv_iff : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
-have a * b * a⁻¹ ≤ a * b * b⁻¹ ↔ a⁻¹ ≤ b⁻¹, from mul_le_mul_iff_left _,
-by { rw [mul_inv_cancel_right, mul_comm a, mul_inv_cancel_right] at this, rw [this] }
+by { rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b], simp }
+
+alias neg_le_neg_iff ↔ le_of_neg_le_neg _
+
+@[to_additive]
+lemma inv_le_of_inv_le (h : a⁻¹ ≤ b) : b⁻¹ ≤ a :=
+inv_le_inv_iff.mp (
+  calc  a⁻¹ ≤ b     : h
+        ... = b⁻¹⁻¹ : (inv_inv _).symm)
 
 @[to_additive neg_le]
 lemma inv_le' : a⁻¹ ≤ b ↔ b⁻¹ ≤ a :=
-have a⁻¹ ≤ (b⁻¹)⁻¹ ↔ b⁻¹ ≤ a, from inv_le_inv_iff,
-by rwa inv_inv at this
+by rw [← inv_le_inv_iff, inv_inv]
 
 @[to_additive le_neg]
 lemma le_inv' : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
-have (a⁻¹)⁻¹ ≤ b⁻¹ ↔ b ≤ a⁻¹, from inv_le_inv_iff,
-by rwa inv_inv at this
+by rw [← inv_le_inv_iff, inv_inv]
 
-@[to_additive neg_le_iff_add_nonneg]
-lemma inv_le_iff_one_le_mul : a⁻¹ ≤ b ↔ 1 ≤ b * a :=
-(mul_le_mul_iff_right a).symm.trans $ by rw inv_mul_self
+@[to_additive]
+lemma mul_inv_le_inv_mul_iff : a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b :=
+by rw [← mul_le_mul_iff_left d, ← mul_le_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
+    inv_mul_cancel_right]
 
-@[to_additive neg_le_iff_add_nonneg']
-lemma inv_le_iff_one_le_mul' : a⁻¹ ≤ b ↔ 1 ≤ a * b :=
-(mul_le_mul_iff_left a).symm.trans $ by rw mul_inv_self
+@[simp, to_additive] lemma div_le_self_iff (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b :=
+by simp [div_eq_mul_inv]
 
-@[to_additive]
-lemma inv_lt_iff_one_lt_mul : a⁻¹ < b ↔ 1 < b * a :=
-(mul_lt_mul_iff_right a).symm.trans $ by rw inv_mul_self
+alias sub_le_self_iff ↔ _ sub_le_self
+
+end typeclasses_left_right_le
+
+section typeclasses_left_right_lt
+variables [has_lt α] [covariant_class α α (*) (<)] [covariant_class α α (function.swap (*)) (<)]
+  {a b c d : α}
+
+@[simp, to_additive]
+lemma inv_lt_inv_iff : a⁻¹ < b⁻¹ ↔ b < a :=
+by { rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b], simp }
 
 @[to_additive]
-lemma inv_lt_iff_one_lt_mul' : a⁻¹ < b ↔ 1 < a * b :=
-(mul_lt_mul_iff_left a).symm.trans $ by rw mul_inv_self
+lemma lt_inv_of_lt_inv (h : a < b⁻¹) : b < a⁻¹ :=
+inv_lt_inv_iff.mp (
+  calc  a⁻¹⁻¹ = a   : inv_inv a
+          ... < b⁻¹ : h)
 
 @[to_additive]
-lemma le_inv_iff_mul_le_one : a ≤ b⁻¹ ↔ a * b ≤ 1 :=
-(mul_le_mul_iff_right b).symm.trans $ by rw inv_mul_self
+lemma inv_lt_of_inv_lt (h : a⁻¹ < b) : b⁻¹ < a :=
+inv_lt_inv_iff.mp (
+    calc  a⁻¹ < b : h
+          ... = b⁻¹⁻¹   : (inv_inv b).symm)
+
+@[to_additive neg_lt]
+lemma inv_lt' : a⁻¹ < b ↔ b⁻¹ < a :=
+by rw [← inv_lt_inv_iff, inv_inv]
+
+@[to_additive lt_neg]
+lemma lt_inv' : a < b⁻¹ ↔ b < a⁻¹ :=
+by rw [← inv_lt_inv_iff, inv_inv]
 
 @[to_additive]
-lemma le_inv_iff_mul_le_one' : a ≤ b⁻¹ ↔ b * a ≤ 1 :=
-(mul_le_mul_iff_left b).symm.trans $ by rw mul_inv_self
+lemma mul_inv_lt_inv_mul_iff : a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b :=
+by rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
+    inv_mul_cancel_right]
+
+@[simp, to_additive] lemma div_lt_self_iff (a : α) {b : α} : a / b < a ↔ 1 < b :=
+by simp [div_eq_mul_inv]
+
+alias sub_lt_self_iff ↔ _ sub_lt_self
+
+end typeclasses_left_right_lt
+
+section pre_order
+variable [preorder α]
+
+section left_le
+variables [covariant_class α α (*) (≤)] {a : α}
 
 @[to_additive]
-lemma lt_inv_iff_mul_lt_one : a < b⁻¹ ↔ a * b < 1 :=
-(mul_lt_mul_iff_right b).symm.trans $ by rw inv_mul_self
+lemma left.inv_le_self (h : 1 ≤ a) : a⁻¹ ≤ a :=
+le_trans (left.inv_le_one_iff.mpr h) h
+
+alias left.neg_le_self ← neg_le_self
 
 @[to_additive]
-lemma lt_inv_iff_mul_lt_one' : a < b⁻¹ ↔ b * a < 1 :=
-(mul_lt_mul_iff_left b).symm.trans $ by rw mul_inv_self
+lemma left.self_le_inv (h : a ≤ 1) : a ≤ a⁻¹ :=
+le_trans h (left.one_le_inv_iff.mpr h)
 
-@[simp, to_additive neg_nonpos]
-lemma inv_le_one' : a⁻¹ ≤ 1 ↔ 1 ≤ a :=
-have a⁻¹ ≤ 1⁻¹ ↔ 1 ≤ a, from inv_le_inv_iff,
-by rwa one_inv at this
+end left_le
 
-@[simp, to_additive neg_nonneg]
-lemma one_le_inv' : 1 ≤ a⁻¹ ↔ a ≤ 1 :=
-have 1⁻¹ ≤ a⁻¹ ↔ a ≤ 1, from inv_le_inv_iff,
-by rwa one_inv at this
+section left_lt
+variables [covariant_class α α (*) (<)] {a : α}
 
 @[to_additive]
-lemma inv_le_self (h : 1 ≤ a) : a⁻¹ ≤ a :=
-le_trans (inv_le_one'.2 h) h
+lemma left.inv_lt_self (h : 1 < a) : a⁻¹ < a :=
+(left.inv_lt_one_iff.mpr h).trans h
+
+alias left.neg_lt_self ← neg_lt_self
 
 @[to_additive]
-lemma self_le_inv (h : a ≤ 1) : a ≤ a⁻¹ :=
-le_trans h (one_le_inv'.2 h)
+lemma left.self_lt_inv (h : a < 1) : a < a⁻¹ :=
+lt_trans h (left.one_lt_inv_iff.mpr h)
 
-@[simp, to_additive]
-lemma inv_lt_inv_iff : a⁻¹ < b⁻¹ ↔ b < a :=
-have a * b * a⁻¹ < a * b * b⁻¹ ↔ a⁻¹ < b⁻¹, from mul_lt_mul_iff_left _,
-by { rw [mul_inv_cancel_right, mul_comm a, mul_inv_cancel_right] at this, rw [this] }
+end left_lt
 
-@[to_additive neg_lt_zero]
-lemma inv_lt_one' : a⁻¹ < 1 ↔ 1 < a :=
-have a⁻¹ < 1⁻¹ ↔ 1 < a, from inv_lt_inv_iff,
-by rwa one_inv at this
+section right_le
+variables [covariant_class α α (function.swap (*)) (≤)] {a : α}
 
-@[to_additive neg_pos]
-lemma one_lt_inv' : 1 < a⁻¹ ↔ a < 1 :=
-have 1⁻¹ < a⁻¹ ↔ a < 1, from inv_lt_inv_iff,
-by rwa one_inv at this
+@[to_additive]
+lemma right.inv_le_self (h : 1 ≤ a) : a⁻¹ ≤ a :=
+le_trans (right.inv_le_one_iff.mpr h) h
 
-@[to_additive neg_lt]
-lemma inv_lt' : a⁻¹ < b ↔ b⁻¹ < a :=
-have a⁻¹ < (b⁻¹)⁻¹ ↔ b⁻¹ < a, from inv_lt_inv_iff,
-by rwa inv_inv at this
+@[to_additive]
+lemma right.self_le_inv (h : a ≤ 1) : a ≤ a⁻¹ :=
+le_trans h (right.one_le_inv_iff.mpr h)
 
-@[to_additive lt_neg]
-lemma lt_inv' : a < b⁻¹ ↔ b < a⁻¹ :=
-have (a⁻¹)⁻¹ < b⁻¹ ↔ b < a⁻¹, from inv_lt_inv_iff,
-by rwa inv_inv at this
+end right_le
+
+section right_lt
+variables [covariant_class α α (function.swap (*)) (<)] {a : α}
 
 @[to_additive]
-lemma inv_lt_self (h : 1 < a) : a⁻¹ < a :=
-(inv_lt_one'.2 h).trans h
+lemma right.inv_lt_self (h : 1 < a) : a⁻¹ < a :=
+(right.inv_lt_one_iff.mpr h).trans h
 
 @[to_additive]
-lemma le_inv_mul_iff_mul_le : b ≤ a⁻¹ * c ↔ a * b ≤ c :=
-have a⁻¹ * (a * b) ≤ a⁻¹ * c ↔ a * b ≤ c, from mul_le_mul_iff_left _,
-by rwa inv_mul_cancel_left at this
+lemma right.self_lt_inv (h : a < 1) : a < a⁻¹ :=
+lt_trans h (right.one_lt_inv_iff.mpr h)
 
-@[simp, to_additive]
-lemma inv_mul_le_iff_le_mul : b⁻¹ * a ≤ c ↔ a ≤ b * c :=
-have b⁻¹ * a ≤ b⁻¹ * (b * c) ↔ a ≤ b * c, from mul_le_mul_iff_left _,
-by rwa inv_mul_cancel_left at this
+end right_lt
 
-@[to_additive]
-lemma mul_inv_le_iff_le_mul : a * c⁻¹ ≤ b ↔ a ≤ b * c :=
-by rw [mul_comm a, mul_comm b, inv_mul_le_iff_le_mul]
+end pre_order
 
-@[simp, to_additive]
-lemma mul_inv_le_iff_le_mul' : a * b⁻¹ ≤ c ↔ a ≤ b * c :=
-by rw [← inv_mul_le_iff_le_mul, mul_comm]
+end group
+
+section comm_group
+variables [comm_group α]
+
+section has_le
+variables [has_le α] [covariant_class α α (*) (≤)] {a b c d : α}
 
 @[to_additive]
 lemma inv_mul_le_iff_le_mul' : c⁻¹ * a ≤ b ↔ a ≤ b * c :=
 by rw [inv_mul_le_iff_le_mul, mul_comm]
 
 @[simp, to_additive]
-lemma lt_inv_mul_iff_mul_lt : b < a⁻¹ * c ↔ a * b < c :=
-have a⁻¹ * (a * b) < a⁻¹ * c ↔ a * b < c, from mul_lt_mul_iff_left _,
-by rwa inv_mul_cancel_left at this
+lemma mul_inv_le_iff_le_mul' : a * b⁻¹ ≤ c ↔ a ≤ b * c :=
+by rw [← inv_mul_le_iff_le_mul, mul_comm]
 
-@[simp, to_additive]
-lemma inv_mul_lt_iff_lt_mul : b⁻¹ * a < c ↔ a < b * c :=
-have b⁻¹ * a < b⁻¹ * (b * c) ↔ a < b * c, from mul_lt_mul_iff_left _,
-by rwa inv_mul_cancel_left at this
+@[to_additive add_neg_le_add_neg_iff]
+lemma mul_inv_le_mul_inv_iff' : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b :=
+by rw [mul_comm c, mul_inv_le_inv_mul_iff, mul_comm]
+
+end has_le
+
+section has_lt
+variables [has_lt α] [covariant_class α α (*) (<)] {a b c d : α}
 
 @[to_additive]
-lemma inv_mul_lt_iff_lt_mul_right : c⁻¹ * a < b ↔ a < b * c :=
+lemma inv_mul_lt_iff_lt_mul' : c⁻¹ * a < b ↔ a < b * c :=
 by rw [inv_mul_lt_iff_lt_mul, mul_comm]
 
-@[to_additive add_neg_le_add_neg_iff]
-lemma mul_inv_le_mul_inv_iff' : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b :=
-begin
-  split ; intro h,
-  have := mul_le_mul_right' (mul_le_mul_right' h b) d,
-  rwa [inv_mul_cancel_right, mul_assoc _ _ b, mul_comm _ b, ← mul_assoc, inv_mul_cancel_right]
-    at this,
-  have := mul_le_mul_right' (mul_le_mul_right' h d⁻¹) b⁻¹,
-  rwa [mul_inv_cancel_right, _root_.mul_assoc, _root_.mul_comm d⁻¹ b⁻¹, ← mul_assoc,
-    mul_inv_cancel_right] at this,
-end
+@[simp, to_additive]
+lemma mul_inv_lt_iff_le_mul' : a * b⁻¹ < c ↔ a < b * c :=
+by rw [← inv_mul_lt_iff_lt_mul, mul_comm]
 
-@[simp, to_additive] lemma div_le_self_iff (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b :=
-by simp [div_eq_mul_inv]
+@[to_additive add_neg_lt_add_neg_iff]
+lemma mul_inv_lt_mul_inv_iff' : a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b :=
+by rw [mul_comm c, mul_inv_lt_inv_mul_iff, mul_comm]
 
-@[simp, to_additive] lemma div_lt_self_iff (a : α) {b : α} : a / b < a ↔ 1 < b :=
-by simp [div_eq_mul_inv]
+end has_lt
+
+end comm_group
+
+alias le_inv' ↔ le_inv_of_le_inv _
+attribute [to_additive] le_inv_of_le_inv
+
+alias left.inv_le_one_iff ↔ one_le_of_inv_le_one _
+attribute [to_additive] one_le_of_inv_le_one
+
+alias left.one_le_inv_iff ↔ le_one_of_one_le_inv _
+attribute [to_additive nonpos_of_neg_nonneg] le_one_of_one_le_inv
+
+alias inv_lt_inv_iff ↔ lt_of_inv_lt_inv _
+attribute [to_additive] lt_of_inv_lt_inv
+
+alias left.inv_lt_one_iff ↔ one_lt_of_inv_lt_one _
+attribute [to_additive] one_lt_of_inv_lt_one
+
+alias left.inv_lt_one_iff ← inv_lt_one_iff_one_lt
+attribute [to_additive] inv_lt_one_iff_one_lt
+
+alias left.inv_lt_one_iff ← inv_lt_one'
+attribute [to_additive neg_lt_zero] inv_lt_one'
+
+alias left.one_lt_inv_iff ↔  inv_of_one_lt_inv _
+attribute [to_additive neg_of_neg_pos] inv_of_one_lt_inv
+
+alias left.one_lt_inv_iff ↔ _ one_lt_inv_of_inv
+attribute [to_additive neg_pos_of_neg] one_lt_inv_of_inv
+
+alias le_inv_mul_iff_mul_le ↔ mul_le_of_le_inv_mul _
+attribute [to_additive] mul_le_of_le_inv_mul
+
+alias le_inv_mul_iff_mul_le ↔ _ le_inv_mul_of_mul_le
+attribute [to_additive] le_inv_mul_of_mul_le
+
+alias inv_mul_le_iff_le_mul ↔ _ inv_mul_le_of_le_mul
+attribute [to_additive] inv_mul_le_iff_le_mul
+
+alias lt_inv_mul_iff_mul_lt ↔ mul_lt_of_lt_inv_mul _
+attribute [to_additive] mul_lt_of_lt_inv_mul
+
+alias lt_inv_mul_iff_mul_lt ↔ _ lt_inv_mul_of_mul_lt
+attribute [to_additive] lt_inv_mul_of_mul_lt
+
+alias inv_mul_lt_iff_lt_mul ↔ lt_mul_of_inv_mul_lt inv_mul_lt_of_lt_mul
+attribute [to_additive] lt_mul_of_inv_mul_lt
+attribute [to_additive] inv_mul_lt_of_lt_mul
+
+alias lt_mul_of_inv_mul_lt ← lt_mul_of_inv_mul_lt_left
+attribute [to_additive] lt_mul_of_inv_mul_lt_left
+
+alias left.inv_le_one_iff ← inv_le_one'
+attribute [to_additive neg_nonpos] inv_le_one'
+
+alias left.one_le_inv_iff ← one_le_inv'
+attribute [to_additive neg_nonneg] one_le_inv'
+
+alias left.one_lt_inv_iff ← one_lt_inv'
+attribute [to_additive neg_pos] one_lt_inv'
+
+alias mul_lt_mul_left' ← ordered_comm_group.mul_lt_mul_left'
+attribute [to_additive ordered_add_comm_group.add_lt_add_left] ordered_comm_group.mul_lt_mul_left'
+
+alias le_of_mul_le_mul_left' ← ordered_comm_group.le_of_mul_le_mul_left
+attribute [to_additive ordered_add_comm_group.le_of_add_le_add_left]
+  ordered_comm_group.le_of_mul_le_mul_left
+
+alias lt_of_mul_lt_mul_left' ← ordered_comm_group.lt_of_mul_lt_mul_left
+attribute [to_additive ordered_add_comm_group.lt_of_add_lt_add_left]
+  ordered_comm_group.lt_of_mul_lt_mul_left
 
 /-- Pullback an `ordered_comm_group` under an injective map.
 See note [reducible non-instances]. -/
 @[reducible, to_additive function.injective.ordered_add_comm_group
 "Pullback an `ordered_add_comm_group` under an injective map."]
-def function.injective.ordered_comm_group {β : Type*}
+def function.injective.ordered_comm_group [ordered_comm_group α] {β : Type*}
   [has_one β] [has_mul β] [has_inv β] [has_div β]
   (f : β → α) (hf : function.injective f) (one : f 1 = 1)
   (mul : ∀ x y, f (x * y) = f x * f y)
@@ -443,138 +526,293 @@ def function.injective.ordered_comm_group {β : Type*}
   ..hf.ordered_comm_monoid f one mul,
   ..hf.comm_group f one mul inv div }
 
-end ordered_comm_group
+/-  Most of the lemmas that are primed in this section appear in ordered_field. -/
+/-  I (DT) did not try to minimise the assumptions. -/
+section group
+variables [group α] [has_le α]
 
-section ordered_add_comm_group
-variables [ordered_add_comm_group α] {a b c d : α}
+section right
+variables [covariant_class α α (function.swap (*)) (≤)] {a b c d : α}
 
-lemma sub_le_sub (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c :=
-by simpa only [sub_eq_add_neg] using add_le_add hab (neg_le_neg hcd)
+@[simp, to_additive]
+lemma div_le_div_iff_right (c : α) : a / c ≤ b / c ↔ a ≤ b :=
+by simpa only [div_eq_mul_inv] using mul_le_mul_iff_right _
 
-lemma sub_lt_sub (hab : a < b) (hcd : c < d) : a - d < b - c :=
-by simpa only [sub_eq_add_neg] using add_lt_add hab (neg_lt_neg hcd)
+@[to_additive sub_le_sub_right]
+lemma div_le_div_right' (h : a ≤ b) (c : α) : a / c ≤ b / c :=
+(div_le_div_iff_right c).2 h
 
-alias sub_le_self_iff ↔ _ sub_le_self
+@[simp, to_additive sub_nonneg]
+lemma one_le_div' : 1 ≤ a / b ↔ b ≤ a :=
+by rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
 
-alias sub_lt_self_iff ↔ _ sub_lt_self
+alias sub_nonneg ↔ le_of_sub_nonneg sub_nonneg_of_le
 
-lemma sub_le_sub_iff : a - b ≤ c - d ↔ a + d ≤ c + b :=
-by simpa only [sub_eq_add_neg] using add_neg_le_add_neg_iff
+@[simp, to_additive sub_nonpos]
+lemma div_le_one' : a / b ≤ 1 ↔ a ≤ b :=
+by rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
 
-@[simp]
-lemma sub_le_sub_iff_left (a : α) {b c : α} : a - b ≤ a - c ↔ c ≤ b :=
-by rw [sub_eq_add_neg, sub_eq_add_neg, add_le_add_iff_left, neg_le_neg_iff]
+alias sub_nonpos ↔ le_of_sub_nonpos sub_nonpos_of_le
 
-lemma sub_le_sub_left (h : a ≤ b) (c : α) : c - b ≤ c - a :=
-(sub_le_sub_iff_left c).2 h
+@[to_additive]
+lemma le_div_iff_mul_le : a ≤ c / b ↔ a * b ≤ c :=
+by rw [← mul_le_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]
 
-@[simp]
-lemma sub_le_sub_iff_right (c : α) : a - c ≤ b - c ↔ a ≤ b :=
-by simpa only [sub_eq_add_neg] using add_le_add_iff_right _
+alias le_sub_iff_add_le ↔ add_le_of_le_sub_right le_sub_right_of_add_le
 
-lemma sub_le_sub_right (h : a ≤ b) (c : α) : a - c ≤ b - c :=
-(sub_le_sub_iff_right c).2 h
+@[to_additive]
+lemma div_le_iff_le_mul : a / c ≤ b ↔ a ≤ b * c :=
+by rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
 
-@[simp]
-lemma sub_lt_sub_iff_left (a : α) {b c : α} : a - b < a - c ↔ c < b :=
-by rw [sub_eq_add_neg, sub_eq_add_neg, add_lt_add_iff_left, neg_lt_neg_iff]
+end right
 
-lemma sub_lt_sub_left (h : a < b) (c : α) : c - b < c - a :=
-(sub_lt_sub_iff_left c).2 h
+section left
+variables [covariant_class α α (*) (≤)] [covariant_class α α (function.swap (*)) (≤)] {a b c : α}
 
-@[simp]
-lemma sub_lt_sub_iff_right (c : α) : a - c < b - c ↔ a < b :=
-by simpa only [sub_eq_add_neg] using add_lt_add_iff_right _
+@[simp, to_additive]
+lemma div_le_div_iff_left (a : α) : a / b ≤ a / c ↔ c ≤ b :=
+by rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
+    inv_mul_cancel_left, inv_le_inv_iff]
 
-lemma sub_lt_sub_right (h : a < b) (c : α) : a - c < b - c :=
-(sub_lt_sub_iff_right c).2 h
+@[to_additive sub_le_sub_left]
+lemma div_le_div_left' (h : a ≤ b) (c : α) : c / b ≤ c / a :=
+(div_le_div_iff_left c).2 h
 
-@[simp] lemma sub_nonneg : 0 ≤ a - b ↔ b ≤ a :=
-by rw [← sub_self a, sub_le_sub_iff_left]
+end left
 
-alias sub_nonneg ↔ le_of_sub_nonneg sub_nonneg_of_le
+end group
 
-@[simp] lemma sub_nonpos : a - b ≤ 0 ↔ a ≤ b :=
-by rw [← sub_self b,  sub_le_sub_iff_right]
+section comm_group
+variables [comm_group α]
 
-alias sub_nonpos ↔ le_of_sub_nonpos sub_nonpos_of_le
+section has_le
+variables [has_le α] [covariant_class α α (*) (≤)] {a b c d : α}
 
-@[simp] lemma sub_pos : 0 < a - b ↔ b < a :=
-by rw [← sub_self a, sub_lt_sub_iff_left]
+@[to_additive sub_le_sub_iff]
+lemma div_le_div_iff' : a / b ≤ c / d ↔ a * d ≤ c * b :=
+by simpa only [div_eq_mul_inv] using mul_inv_le_mul_inv_iff'
 
-alias sub_pos ↔ lt_of_sub_pos sub_pos_of_lt
+@[to_additive]
+lemma le_div_iff_mul_le' : b ≤ c / a ↔ a * b ≤ c :=
+by rw [le_div_iff_mul_le, mul_comm]
 
-@[simp] lemma sub_lt_zero : a - b < 0 ↔ a < b :=
-by rw [← sub_self b, sub_lt_sub_iff_right]
+alias le_sub_iff_add_le' ↔ add_le_of_le_sub_left le_sub_left_of_add_le
 
-alias sub_lt_zero ↔ lt_of_sub_neg sub_neg_of_lt
+@[to_additive]
+lemma div_le_iff_le_mul' : a / b ≤ c ↔ a ≤ b * c :=
+by rw [div_le_iff_le_mul, mul_comm]
 
-lemma le_sub_iff_add_le' : b ≤ c - a ↔ a + b ≤ c :=
-by rw [sub_eq_add_neg, add_comm, le_neg_add_iff_add_le]
+alias sub_le_iff_le_add' ↔ le_add_of_sub_left_le sub_left_le_of_le_add
 
-lemma le_sub_iff_add_le : a ≤ c - b ↔ a + b ≤ c :=
-by rw [le_sub_iff_add_le', add_comm]
+@[simp, to_additive]
+lemma inv_le_div_iff_le_mul : b⁻¹ ≤ a / c ↔ c ≤ a * b :=
+le_div_iff_mul_le.trans inv_mul_le_iff_le_mul'
 
-alias le_sub_iff_add_le ↔ add_le_of_le_sub_right le_sub_right_of_add_le
+@[to_additive]
+lemma inv_le_div_iff_le_mul' : a⁻¹ ≤ b / c ↔ c ≤ a * b :=
+by rw [inv_le_div_iff_le_mul, mul_comm]
 
-lemma sub_le_iff_le_add' : a - b ≤ c ↔ a ≤ b + c :=
-by rw [sub_eq_add_neg, add_comm, neg_add_le_iff_le_add]
+@[to_additive sub_le]
+lemma div_le'' : a / b ≤ c ↔ a / c ≤ b :=
+div_le_iff_le_mul'.trans div_le_iff_le_mul.symm
 
-alias le_sub_iff_add_le' ↔ add_le_of_le_sub_left le_sub_left_of_add_le
+@[to_additive le_sub]
+lemma le_div'' : a ≤ b / c ↔ c ≤ b / a :=
+le_div_iff_mul_le'.trans le_div_iff_mul_le.symm
+
+end has_le
 
-lemma sub_le_iff_le_add : a - c ≤ b ↔ a ≤ b + c :=
-by rw [sub_le_iff_le_add', add_comm]
+section preorder
+variables [preorder α] [covariant_class α α (*) (≤)] {a b c d : α}
 
-@[simp] lemma neg_le_sub_iff_le_add : -b ≤ a - c ↔ c ≤ a + b :=
-le_sub_iff_add_le.trans neg_add_le_iff_le_add'
+@[to_additive sub_le_sub]
+lemma div_le_div'' (hab : a ≤ b) (hcd : c ≤ d) :
+  a / d ≤ b / c :=
+begin
+  rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm],
+  exact mul_le_mul' hab hcd
+end
 
-lemma neg_le_sub_iff_le_add' : -a ≤ b - c ↔ c ≤ a + b :=
-by rw [neg_le_sub_iff_le_add, add_comm]
+end preorder
 
-lemma sub_le : a - b ≤ c ↔ a - c ≤ b :=
-sub_le_iff_le_add'.trans sub_le_iff_le_add.symm
+end comm_group
 
-theorem le_sub : a ≤ b - c ↔ c ≤ b - a :=
-le_sub_iff_add_le'.trans le_sub_iff_add_le.symm
+/-  Most of the lemmas that are primed in this section appear in ordered_field. -/
+/-  I (DT) did not try to minimise the assumptions. -/
+section group
+variables [group α] [has_lt α]
 
-lemma lt_sub_iff_add_lt' : b < c - a ↔ a + b < c :=
-by rw [sub_eq_add_neg, add_comm, lt_neg_add_iff_add_lt]
+section right
+variables [covariant_class α α (function.swap (*)) (<)] {a b c d : α}
 
-alias lt_sub_iff_add_lt' ↔ add_lt_of_lt_sub_left lt_sub_left_of_add_lt
+@[simp, to_additive]
+lemma div_lt_div_iff_right (c : α) : a / c < b / c ↔ a < b :=
+by simpa only [div_eq_mul_inv] using mul_lt_mul_iff_right _
+
+@[to_additive sub_lt_sub_right]
+lemma div_lt_div_right' (h : a < b) (c : α) : a / c < b / c :=
+(div_lt_div_iff_right c).2 h
+
+@[simp, to_additive sub_pos]
+lemma one_lt_div' : 1 < a / b ↔ b < a :=
+by rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
+
+alias sub_pos ↔ lt_of_sub_pos sub_pos_of_lt
+
+@[simp, to_additive sub_neg]
+lemma div_lt_one' : a / b < 1 ↔ a < b :=
+by rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
 
-lemma lt_sub_iff_add_lt : a < c - b ↔ a + b < c :=
-by rw [lt_sub_iff_add_lt', add_comm]
+alias sub_neg ↔ lt_of_sub_neg sub_neg_of_lt
+
+alias sub_neg ← sub_lt_zero
+
+@[to_additive]
+lemma lt_div_iff_mul_lt : a < c / b ↔ a * b < c :=
+by rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]
 
 alias lt_sub_iff_add_lt ↔ add_lt_of_lt_sub_right lt_sub_right_of_add_lt
 
-lemma sub_lt_iff_lt_add' : a - b < c ↔ a < b + c :=
-by rw [sub_eq_add_neg, add_comm, neg_add_lt_iff_lt_add]
+@[to_additive]
+lemma div_lt_iff_lt_mul : a / c < b ↔ a < b * c :=
+by rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
+
+alias sub_lt_iff_lt_add ↔ lt_add_of_sub_right_lt sub_right_lt_of_lt_add
+
+end right
+
+section left
+variables [covariant_class α α (*) (<)] [covariant_class α α (function.swap (*)) (<)] {a b c : α}
+
+@[simp, to_additive]
+lemma div_lt_div_iff_left (a : α) : a / b < a / c ↔ c < b :=
+by rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
+    inv_mul_cancel_left, inv_lt_inv_iff]
+
+@[simp, to_additive]
+lemma inv_lt_div_iff_lt_mul : a⁻¹ < b / c ↔ c < a * b :=
+by rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]
+
+@[to_additive sub_lt_sub_left]
+lemma div_lt_div_left' (h : a < b) (c : α) : c / b < c / a :=
+(div_lt_div_iff_left c).2 h
+
+end left
+
+end group
+
+section comm_group
+variables [comm_group α]
+
+section has_lt
+variables [has_lt α] [covariant_class α α (*) (<)] {a b c d : α}
+
+@[to_additive sub_lt_sub_iff]
+lemma div_lt_div_iff' : a / b < c / d ↔ a * d < c * b :=
+by simpa only [div_eq_mul_inv] using mul_inv_lt_mul_inv_iff'
+
+@[to_additive]
+lemma lt_div_iff_mul_lt' : b < c / a ↔ a * b < c :=
+by rw [lt_div_iff_mul_lt, mul_comm]
+
+alias lt_sub_iff_add_lt' ↔ add_lt_of_lt_sub_left lt_sub_left_of_add_lt
+
+@[to_additive]
+lemma div_lt_iff_lt_mul' : a / b < c ↔ a < b * c :=
+by rw [div_lt_iff_lt_mul, mul_comm]
 
 alias sub_lt_iff_lt_add' ↔ lt_add_of_sub_left_lt sub_left_lt_of_lt_add
 
-lemma sub_lt_iff_lt_add : a - c < b ↔ a < b + c :=
-by rw [sub_lt_iff_lt_add', add_comm]
+@[to_additive]
+lemma inv_lt_div_iff_lt_mul' : b⁻¹ < a / c ↔ c < a * b :=
+lt_div_iff_mul_lt.trans inv_mul_lt_iff_lt_mul'
 
-alias sub_lt_iff_lt_add ↔ lt_add_of_sub_right_lt sub_right_lt_of_lt_add
+@[to_additive sub_lt]
+lemma div_lt'' : a / b < c ↔ a / c < b :=
+div_lt_iff_lt_mul'.trans div_lt_iff_lt_mul.symm
 
-@[simp] lemma neg_lt_sub_iff_lt_add : -b < a - c ↔ c < a + b :=
-lt_sub_iff_add_lt.trans neg_add_lt_iff_lt_add_right
+@[to_additive lt_sub]
+lemma lt_div'' : a < b / c ↔ c < b / a :=
+lt_div_iff_mul_lt'.trans lt_div_iff_mul_lt.symm
 
-lemma neg_lt_sub_iff_lt_add' : -a < b - c ↔ c < a + b :=
-by rw [neg_lt_sub_iff_lt_add, add_comm]
+end has_lt
 
-lemma sub_lt : a - b < c ↔ a - c < b :=
-sub_lt_iff_lt_add'.trans sub_lt_iff_lt_add.symm
+section preorder
+variables [preorder α] [covariant_class α α (*) (<)] {a b c d : α}
 
-theorem lt_sub : a < b - c ↔ c < b - a :=
-lt_sub_iff_add_lt'.trans lt_sub_iff_add_lt.symm
+@[to_additive sub_lt_sub]
+lemma div_lt_div'' (hab : a < b) (hcd : c < d) :
+  a / d < b / c :=
+begin
+  rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm],
+  exact mul_lt_mul_of_lt_of_lt hab hcd
+end
 
-end ordered_add_comm_group
+end preorder
 
-/-!
+end comm_group
 
-### Linearly ordered commutative groups
+section linear_order
+variables [group α] [linear_order α] [covariant_class α α (*) (≤)]
+
+section variable_names
+variables {a b c : α}
+
+@[to_additive]
+lemma le_of_forall_one_lt_lt_mul (h : ∀ ε : α, 1 < ε → a < b * ε) : a ≤ b :=
+le_of_not_lt (λ h₁, lt_irrefl a (by simpa using (h _ (lt_inv_mul_iff_lt.mpr h₁))))
+
+@[to_additive]
+lemma le_iff_forall_one_lt_lt_mul : a ≤ b ↔ ∀ ε, 1 < ε → a < b * ε :=
+⟨λ h ε, lt_mul_of_le_of_one_lt h, le_of_forall_one_lt_lt_mul⟩
+
+/-  I (DT) introduced this lemma to prove (the additive version `sub_le_sub_flip` of)
+`div_le_div_flip` below.  Now I wonder what is the point of either of these lemmas... -/
+@[to_additive]
+lemma div_le_inv_mul_iff [covariant_class α α (function.swap (*)) (≤)] :
+  a / b ≤ a⁻¹ * b ↔ a ≤ b :=
+begin
+  rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff],
+  exact ⟨λ h, not_lt.mp (λ k, not_lt.mpr h (mul_lt_mul''' k k)), λ h, mul_le_mul' h h⟩,
+end
+
+/-  What is the point of this lemma?  See comment about `div_le_inv_mul_iff` above. -/
+@[simp, to_additive]
+lemma div_le_div_flip {α : Type*} [comm_group α] [linear_order α] [covariant_class α α (*) (≤)]
+  {a b : α}:
+  a / b ≤ b / a ↔ a ≤ b :=
+begin
+  rw [div_eq_mul_inv b, mul_comm],
+  exact div_le_inv_mul_iff,
+end
+
+@[simp, to_additive] lemma max_one_div_max_inv_one_eq_self (a : α) :
+  max a 1 / max a⁻¹ 1 = a :=
+by { rcases le_total a 1 with h|h; simp [h] }
+
+alias max_zero_sub_max_neg_zero_eq_self ← max_zero_sub_eq_self
+
+end variable_names
+
+section densely_ordered
+variables [densely_ordered α] {a b c : α}
+
+@[to_additive]
+lemma le_of_forall_one_lt_le_mul (h : ∀ ε : α, 1 < ε → a ≤ b * ε) : a ≤ b :=
+le_of_forall_le_of_dense $ λ c hc,
+calc a ≤ b * (b⁻¹ * c) : h _ (lt_inv_mul_iff_lt.mpr hc)
+   ... = c            : mul_inv_cancel_left b c
 
+@[to_additive]
+lemma le_iff_forall_one_lt_le_mul : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε :=
+⟨λ h ε ε_pos, le_mul_of_le_of_one_le h ε_pos.le, le_of_forall_one_lt_le_mul⟩
+
+end densely_ordered
+
+end linear_order
+
+/-!
+### Linearly ordered commutative groups
 -/
 
 /-- A linearly ordered additive commutative group is an
@@ -628,11 +866,11 @@ mul_lt_mul_left' h c
 
 @[to_additive min_neg_neg]
 lemma min_inv_inv' (a b : α) : min (a⁻¹) (b⁻¹) = (max a b)⁻¹ :=
-eq.symm $ @monotone.map_max α (order_dual α) _ _ has_inv.inv a b $ λ a b, inv_le_inv'
+eq.symm $ @monotone.map_max α (order_dual α) _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
 
 @[to_additive max_neg_neg]
 lemma max_inv_inv' (a b : α) : max (a⁻¹) (b⁻¹) = (min a b)⁻¹ :=
-eq.symm $ @monotone.map_min α (order_dual α) _ _ has_inv.inv a b $ λ a b, inv_le_inv'
+eq.symm $ @monotone.map_min α (order_dual α) _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
 
 @[to_additive min_sub_sub_right]
 lemma min_div_div_right' (a b c : α) : min (a / c) (b / c) = min a b / c :=
@@ -650,15 +888,6 @@ by simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']
 lemma max_div_div_left' (a b c : α) : max (a / b) (a / c) = a / min b c :=
 by simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']
 
-@[to_additive max_zero_sub_eq_self]
-lemma max_one_div_eq_self' (a : α) : max a 1 / max (a⁻¹) 1 = a :=
-begin
-  rcases le_total a 1,
-  { rw [max_eq_right h, max_eq_left, one_div, inv_inv], { rwa [le_inv', one_inv] } },
-  { rw [max_eq_left, max_eq_right, div_eq_mul_inv, one_inv, mul_one],
-    { rwa [inv_le', one_inv] }, exact h }
-end
-
 @[to_additive eq_zero_of_neg_eq]
 lemma eq_one_of_inv_eq' (h : a⁻¹ = a) : a = 1 :=
 match lt_trichotomy a 1 with
@@ -667,7 +896,7 @@ match lt_trichotomy a 1 with
   absurd h₁ this.asymm
 | or.inr (or.inl h₁) := h₁
 | or.inr (or.inr h₁) :=
-  have a < 1, from h ▸ inv_inv_of_one_lt h₁,
+  have a < 1, from h ▸ inv_lt_one'.mpr h₁,
   absurd h₁ this.asymm
 end
 
@@ -697,46 +926,56 @@ instance linear_ordered_comm_group.to_no_bot_order [nontrivial α] : no_bot_orde
 
 end linear_ordered_comm_group
 
-section linear_ordered_add_comm_group
+section covariant_add_le
 
-variables [linear_ordered_add_comm_group α] {a b c : α}
+section has_neg
+variables [has_neg α] [linear_order α] {a b: α}
 
-@[simp]
-lemma sub_le_sub_flip : a - b ≤ b - a ↔ a ≤ b :=
-begin
-  rw [sub_le_iff_le_add, sub_add_eq_add_sub, le_sub_iff_add_le],
-  split,
-  { intro h,
-    by_contra H,
-    rw not_le at H,
-    apply not_lt.2 h,
-    exact add_lt_add H H, },
-  { intro h,
-    exact add_le_add h h, }
-end
+/-- `abs a` is the absolute value of `a`. -/
+def abs {α : Type*} [has_neg α] [linear_order α] (a : α) : α := max a (-a)
 
-@[simp] lemma max_zero_sub_max_neg_zero_eq_self (a : α) :
-  max a 0 - max (-a) 0 = a :=
-by { rcases le_total a 0 with h|h; simp [h] }
+lemma abs_choice (x : α) : abs x = x ∨ abs x = -x := max_choice _ _
 
-lemma le_of_forall_pos_le_add [densely_ordered α] (h : ∀ ε : α, 0 < ε → a ≤ b + ε) : a ≤ b :=
-le_of_forall_le_of_dense $ λ c hc,
-calc a ≤ b + (c - b) : h _ (sub_pos_of_lt hc)
-   ... = c           : add_sub_cancel'_right _ _
+lemma abs_le' : abs a ≤ b ↔ a ≤ b ∧ -a ≤ b := max_le_iff
 
-lemma le_iff_forall_pos_le_add [densely_ordered α] : a ≤ b ↔ ∀ ε, 0 < ε → a ≤ b + ε :=
-⟨λ h ε ε_pos, le_add_of_le_of_nonneg h ε_pos.le, le_of_forall_pos_le_add⟩
+lemma le_abs : a ≤ abs b ↔ a ≤ b ∨ a ≤ -b := le_max_iff
 
-lemma le_of_forall_pos_lt_add (h : ∀ ε : α, 0 < ε → a < b + ε) : a ≤ b :=
-le_of_not_lt $ λ h₁, by simpa using h _ (sub_pos_of_lt h₁)
+lemma le_abs_self (a : α) : a ≤ abs a := le_max_left _ _
 
-lemma le_iff_forall_pos_lt_add : a ≤ b ↔ ∀ ε, 0 < ε → a < b + ε :=
-⟨λ h ε, lt_add_of_le_of_pos h, le_of_forall_pos_lt_add⟩
+lemma neg_le_abs_self (a : α) : -a ≤ abs a := le_max_right _ _
 
-/-- `abs a` is the absolute value of `a`. -/
-def abs (a : α) : α := max a (-a)
+lemma lt_abs : a < abs b ↔ a < b ∨ a < -b := lt_max_iff
 
-lemma abs_choice (x : α) : abs x = x ∨ abs x = -x := max_choice _ _
+theorem abs_le_abs (h₀ : a ≤ b) (h₁ : -a ≤ b) : abs a ≤ abs b :=
+(abs_le'.2 ⟨h₀, h₁⟩).trans (le_abs_self b)
+
+lemma abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P (abs a) :=
+sup_ind _ _ h1 h2
+
+end has_neg
+
+section add_group
+variables [add_group α] [linear_order α]
+
+@[simp] lemma abs_neg (a : α) : abs (-a) = abs a :=
+begin unfold abs, rw [max_comm, neg_neg] end
+
+lemma eq_or_eq_neg_of_abs_eq {a b : α} (h : abs a = b) : a = b ∨ a = -b :=
+by simpa only [← h, eq_comm, eq_neg_iff_eq_neg] using abs_choice a
+
+lemma abs_eq_abs {a b : α} : abs a = abs b ↔ a = b ∨ a = -b :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { obtain rfl | rfl := eq_or_eq_neg_of_abs_eq h;
+    simpa only [neg_eq_iff_neg_eq, neg_inj, or.comm, @eq_comm _ (-b)] using abs_choice b },
+  { cases h; simp only [h, abs_neg] },
+end
+
+lemma abs_sub_comm (a b : α) : abs (a - b) = abs (b - a) :=
+calc  abs (a - b) = abs (- (b - a)) : congr_arg _ (neg_sub b a).symm
+              ... = abs (b - a)     : abs_neg (b - a)
+
+variables [covariant_class α α (+) (≤)] {a b c : α}
 
 lemma abs_of_nonneg (h : 0 ≤ a) : abs a = a :=
 max_eq_left $ (neg_nonpos.2 h).trans h
@@ -753,9 +992,6 @@ abs_of_nonpos h.le
 @[simp] lemma abs_zero : abs 0 = (0:α) :=
 abs_of_nonneg le_rfl
 
-@[simp] lemma abs_neg (a : α) : abs (-a) = abs a :=
-begin unfold abs, rw [max_comm, neg_neg] end
-
 @[simp] lemma abs_pos : 0 < abs a ↔ a ≠ 0 :=
 begin
   rcases lt_trichotomy a 0 with (ha|rfl|ha),
@@ -768,26 +1004,15 @@ lemma abs_pos_of_pos (h : 0 < a) : 0 < abs a := abs_pos.2 h.ne.symm
 
 lemma abs_pos_of_neg (h : a < 0) : 0 < abs a := abs_pos.2 h.ne
 
-lemma abs_sub_comm (a b : α) : abs (a - b) = abs (b - a) :=
-by rw [← neg_sub, abs_neg]
-
-lemma abs_le' : abs a ≤ b ↔ a ≤ b ∧ -a ≤ b := max_le_iff
-
-lemma abs_le : abs a ≤ b ↔ - b ≤ a ∧ a ≤ b :=
-by rw [abs_le', and.comm, neg_le]
-
-lemma neg_le_of_abs_le (h : abs a ≤ b) : -b ≤ a := (abs_le.mp h).1
-
-lemma le_of_abs_le (h : abs a ≤ b) : a ≤ b := (abs_le.mp h).2
-
-lemma le_abs : a ≤ abs b ↔ a ≤ b ∨ a ≤ -b := le_max_iff
-
-lemma le_abs_self (a : α) : a ≤ abs a := le_max_left _ _
-
-lemma neg_le_abs_self (a : α) : -a ≤ abs a := le_max_right _ _
-
 lemma neg_abs_le_self (a : α) : -abs a ≤ a :=
-neg_le.mpr $ neg_le_abs_self a
+begin
+  cases le_total 0 a with h h,
+  { calc -abs a = - a   : congr_arg (has_neg.neg) (abs_of_nonneg h)
+            ... ≤ 0     : neg_nonpos.mpr h
+            ... ≤ a     : h },
+  { calc -abs a = - - a : congr_arg (has_neg.neg) (abs_of_nonpos h)
+            ... ≤ a     : (neg_neg a).le }
+end
 
 lemma abs_nonneg (a : α) : 0 ≤ abs a :=
 (le_total 0 a).elim (λ h, h.trans (le_abs_self a)) (λ h, (neg_nonneg.2 h).trans $ neg_le_abs_self a)
@@ -801,6 +1026,8 @@ decidable.not_iff_not.1 $ ne_comm.trans $ (abs_nonneg a).lt_iff_ne.symm.trans ab
 @[simp] lemma abs_nonpos_iff {a : α} : abs a ≤ 0 ↔ a = 0 :=
 (abs_nonneg a).le_iff_eq.trans abs_eq_zero
 
+variable [covariant_class α α (function.swap (+)) (≤)]
+
 lemma abs_lt : abs a < b ↔ - b < a ∧ a < b :=
 max_lt_iff.trans $ and.comm.trans $ by rw [neg_lt]
 
@@ -808,8 +1035,6 @@ lemma neg_lt_of_abs_lt (h : abs a < b) : -b < a := (abs_lt.mp h).1
 
 lemma lt_of_abs_lt (h : abs a < b) : a < b := (abs_lt.mp h).2
 
-lemma lt_abs : a < abs b ↔ a < b ∨ a < -b := lt_max_iff
-
 lemma max_sub_min_eq_abs' (a b : α) : max a b - min a b = abs (a - b) :=
 begin
   cases le_total a b with ab ba,
@@ -820,6 +1045,18 @@ end
 lemma max_sub_min_eq_abs (a b : α) : max a b - min a b = abs (b - a) :=
 by { rw abs_sub_comm, exact max_sub_min_eq_abs' _ _ }
 
+end add_group
+
+section add_comm_group
+variables [add_comm_group α] [linear_order α] [covariant_class α α (+) (≤)] {a b c d : α}
+
+lemma abs_le : abs a ≤ b ↔ - b ≤ a ∧ a ≤ b :=
+by rw [abs_le', and.comm, neg_le]
+
+lemma neg_le_of_abs_le (h : abs a ≤ b) : -b ≤ a := (abs_le.mp h).1
+
+lemma le_of_abs_le (h : abs a ≤ b) : a ≤ b := (abs_le.mp h).2
+
 /--
 The **triangle inequality** in `linear_ordered_add_comm_group`s.
 -/
@@ -833,10 +1070,10 @@ theorem abs_sub (a b : α) :
 by { rw [sub_eq_add_neg, ←abs_neg b], exact abs_add a _ }
 
 lemma abs_sub_le_iff : abs (a - b) ≤ c ↔ a - b ≤ c ∧ b - a ≤ c :=
-by rw [abs_le, neg_le_sub_iff_le_add, @sub_le_iff_le_add' _ _ b, and_comm]
+by rw [abs_le, neg_le_sub_iff_le_add, sub_le_iff_le_add', and_comm, sub_le_iff_le_add']
 
 lemma abs_sub_lt_iff : abs (a - b) < c ↔ a - b < c ∧ b - a < c :=
-by rw [abs_lt, neg_lt_sub_iff_lt_add, @sub_lt_iff_lt_add' _ _ b, and_comm]
+by rw [abs_lt, neg_lt_sub_iff_lt_add', sub_lt_iff_lt_add', and_comm, sub_lt_iff_lt_add']
 
 lemma sub_le_of_abs_sub_le_left (h : abs (a - b) ≤ c) : b - c ≤ a :=
 sub_le.1 $ (abs_sub_le_iff.1 h).2
@@ -858,44 +1095,20 @@ calc abs a = abs (a - b + b)     : by rw [sub_add_cancel]
 lemma abs_abs_sub_abs_le_abs_sub (a b : α) : abs (abs a - abs b) ≤ abs (a - b) :=
 abs_sub_le_iff.2 ⟨abs_sub_abs_le_abs_sub _ _, by rw abs_sub_comm; apply abs_sub_abs_le_abs_sub⟩
 
-lemma eq_or_eq_neg_of_abs_eq (h : abs a = b) : a = b ∨ a = -b :=
-by simpa only [← h, eq_comm, eq_neg_iff_eq_neg] using abs_choice a
-
 lemma abs_eq (hb : 0 ≤ b) : abs a = b ↔ a = b ∨ a = -b :=
 begin
   refine ⟨eq_or_eq_neg_of_abs_eq, _⟩,
   rintro (rfl|rfl); simp only [abs_neg, abs_of_nonneg hb]
 end
 
-lemma abs_eq_abs : abs a = abs b ↔ a = b ∨ a = -b :=
-begin
-  refine ⟨λ h, _, λ h, _⟩,
-  { obtain rfl | rfl := eq_or_eq_neg_of_abs_eq h;
-    simpa only [neg_eq_iff_neg_eq, neg_inj, or.comm, @eq_comm _ (-b)] using abs_choice b },
-  { cases h; simp only [h, abs_neg] },
-end
-
 lemma abs_le_max_abs_abs (hab : a ≤ b)  (hbc : b ≤ c) : abs b ≤ max (abs a) (abs c) :=
 abs_le'.2
   ⟨by simp [hbc.trans (le_abs_self c)],
-   by simp [(neg_le_neg hab).trans (neg_le_abs_self a)]⟩
-
-theorem abs_le_abs (h₀ : a ≤ b) (h₁ : -a ≤ b) : abs a ≤ abs b :=
-(abs_le'.2 ⟨h₀, h₁⟩).trans (le_abs_self b)
-
-lemma abs_max_sub_max_le_abs (a b c : α) : abs (max a c - max b c) ≤ abs (a - b) :=
-begin
-  simp_rw [abs_le, le_sub_iff_add_le, sub_le_iff_le_add, ← max_add_add_left],
-  split; apply max_le_max; simp only [← le_sub_iff_add_le, ← sub_le_iff_le_add, sub_self, neg_le,
-    neg_le_abs_self, neg_zero, abs_nonneg, le_abs_self]
-end
+   by simp [(neg_le_neg_iff.mpr hab).trans (neg_le_abs_self a)]⟩
 
 lemma eq_of_abs_sub_eq_zero {a b : α} (h : abs (a - b) = 0) : a = b :=
 sub_eq_zero.1 $ abs_eq_zero.1 h
 
-lemma abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P (abs a) :=
-sup_ind _ _ h1 h2
-
 lemma abs_sub_le (a b c : α) : abs (a - c) ≤ abs (a - b) + abs (b - c) :=
 calc
     abs (a - c) = abs (a - b + (b - c))     : by rw [sub_add_sub_cancel]
@@ -911,14 +1124,28 @@ abs_sub_le_iff.2 ⟨sub_le_sub hau hbl, sub_le_sub hbu hal⟩
 lemma eq_of_abs_sub_nonpos (h : abs (a - b) ≤ 0) : a = b :=
 eq_of_abs_sub_eq_zero (le_antisymm h (abs_nonneg (a - b)))
 
+lemma abs_max_sub_max_le_abs (a b c : α) : abs (max a c - max b c) ≤ abs (a - b) :=
+begin
+  simp_rw [abs_le, le_sub_iff_add_le, sub_le_iff_le_add, ← max_add_add_left],
+  split; apply max_le_max; simp only [← le_sub_iff_add_le, ← sub_le_iff_le_add, sub_self, neg_le,
+    neg_le_abs_self, neg_zero, abs_nonneg, le_abs_self]
+end
+
+end add_comm_group
+
+end covariant_add_le
+
+section linear_ordered_add_comm_group
+variable [linear_ordered_add_comm_group α]
+
 instance with_top.linear_ordered_add_comm_group_with_top :
   linear_ordered_add_comm_group_with_top (with_top α) :=
-{ neg := option.map (λ a : α, -a),
-  neg_top := @option.map_none _ _ (λ a : α, -a),
+{ neg            := option.map (λ a : α, -a),
+  neg_top        := @option.map_none _ _ (λ a : α, -a),
   add_neg_cancel := begin
     rintro (a | a) ha,
     { exact (ha rfl).elim },
-    exact with_top.coe_add.symm.trans (with_top.coe_eq_coe.2 (add_neg_self a)),
+    { exact with_top.coe_add.symm.trans (with_top.coe_eq_coe.2 (add_neg_self a)) }
   end,
   .. with_top.linear_ordered_add_comm_monoid_with_top,
   .. option.nontrivial }
@@ -928,11 +1155,11 @@ end linear_ordered_add_comm_group
 /-- This is not so much a new structure as a construction mechanism
   for ordered groups, by specifying only the "positive cone" of the group. -/
 class nonneg_add_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          : α → 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_add_comm_group
@@ -941,15 +1168,15 @@ include s
 
 @[reducible, priority 100] -- see Note [lower instance priority]
 instance to_ordered_add_comm_group : ordered_add_comm_group α :=
-{ le := λ a b, nonneg (b - a),
-  lt := λ a b, pos (b - a),
+{ 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];
+  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 $
+  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 simpa [(≤), preorder.le] using nab,
+  add_le_add_left  := λ a b nab c, by simpa [(≤), preorder.le] using nab,
   ..s }
 
 theorem nonneg_def {a : α} : nonneg a ↔ 0 ≤ a :=
@@ -1034,3 +1261,32 @@ instance [linear_ordered_comm_group α] : linear_ordered_add_comm_group (additiv
   ..additive.ordered_add_comm_group }
 
 end type_tags
+
+section norm_num_lemmas
+/- The following lemmas are stated so that the `norm_num` tactic can use them with the
+expected signatures.  -/
+variables [ordered_comm_group α] {a b : α}
+
+@[to_additive neg_le_neg]
+lemma inv_le_inv' : a ≤ b → b⁻¹ ≤ a⁻¹ :=
+inv_le_inv_iff.mpr
+
+@[to_additive neg_lt_neg]
+lemma inv_lt_inv' : a < b → b⁻¹ < a⁻¹ :=
+inv_lt_inv_iff.mpr
+
+/-  The additive version is also a `linarith` lemma. -/
+@[to_additive]
+theorem inv_lt_one_of_one_lt : 1 < a → a⁻¹ < 1 :=
+inv_lt_one_iff_one_lt.mpr
+
+/-  The additive version is also a `linarith` lemma. -/
+@[to_additive]
+lemma inv_le_one_of_one_le : 1 ≤ a → a⁻¹ ≤ 1 :=
+inv_le_one'.mpr
+
+@[to_additive neg_nonneg_of_nonpos]
+lemma one_le_inv_of_le_one :  a ≤ 1 → 1 ≤ a⁻¹ :=
+one_le_inv'.mpr
+
+end norm_num_lemmas
diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
index 8468532438eea..9cbcf6fe88f31 100644
--- a/src/analysis/analytic/basic.lean
+++ b/src/analysis/analytic/basic.lean
@@ -427,7 +427,7 @@ begin
   suffices : ∥p.partial_sum n y - f (x + y)∥ ≤ C * (a * (∥y∥ / r')) ^ n / (1 - a * (∥y∥ / r')),
   { refine this.trans _,
     apply_rules [div_le_div_of_le_left, sub_pos.2, div_nonneg, mul_nonneg, pow_nonneg, hC.lt.le,
-      ha.1.le, norm_nonneg, nnreal.coe_nonneg, ha.2, (sub_le_sub_iff_left _).2] },
+      ha.1.le, norm_nonneg, nnreal.coe_nonneg, ha.2, (sub_le_sub_iff_left _).2]; apply_instance },
   apply norm_sub_le_of_geometric_bound_of_has_sum (ya.trans_lt ha.2) _ (hf.has_sum this),
   assume n,
   calc ∥(p n) (λ (i : fin n), y)∥ ≤ ∥p n∥ * (∏ i : fin n, ∥y∥) :
diff --git a/src/topology/algebra/ordered/basic.lean b/src/topology/algebra/ordered/basic.lean
index 9c08b3a1c730f..d57990355a4e8 100644
--- a/src/topology/algebra/ordered/basic.lean
+++ b/src/topology/algebra/ordered/basic.lean
@@ -1494,7 +1494,7 @@ local notation `|` x `|` := abs x
 lemma nhds_eq_infi_abs_sub (a : α) : 𝓝 a = (⨅r>0, 𝓟 {b | |a - b| < r}) :=
 begin
   simp only [le_antisymm_iff, nhds_eq_order, le_inf_iff, le_infi_iff, le_principal_iff, mem_Ioi,
-    mem_Iio, abs_sub_lt_iff, @sub_lt_iff_lt_add _ _ _ _ a, @sub_lt _ _ a, set_of_and],
+    mem_Iio, abs_sub_lt_iff, @sub_lt_iff_lt_add _ _ _ _ _ _ a, @sub_lt _ _ _ _ a, set_of_and],
   refine ⟨_, _, _⟩,
   { intros ε ε0,
     exact inter_mem_inf_sets
@@ -1580,7 +1580,7 @@ begin
   convert nhds_basis_Ioo_pos a,
   { ext ε,
     change abs (x - a) < ε ↔ a - ε < x ∧ x < a + ε,
-    simp [abs_lt, sub_lt_iff_lt_add, add_comm ε a] },
+    simp [abs_lt, sub_lt_iff_lt_add, add_comm ε a, add_comm x ε] }
 end
 
 variable (α)