diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean
index 0875bfad39..51969023de 100644
--- a/library/init/algebra/functions.lean
+++ b/library/init/algebra/functions.lean
@@ -247,7 +247,7 @@ abs_of_nonneg $ abs_nonneg a
 lemma le_abs_self (a : α) : a ≤ abs a :=
 or.elim (le_total 0 a)
   (assume h : 0 ≤ a,
-   begin rw [abs_of_nonneg h], apply le_refl end)
+   begin rw [abs_of_nonneg h] end)
   (assume h : a ≤ 0, le_trans h $ abs_nonneg a)
 
 lemma neg_le_abs_self (a : α) : -a ≤ abs a :=
diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean
index edfcd725ed..a1e395a204 100644
--- a/library/init/algebra/order.lean
+++ b/library/init/algebra/order.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.logic
+import init.logic init.classical
 /- Make sure instances defined in this file have lower priority than the ones
    defined for concrete structures -/
 set_option default_priority 100
@@ -14,165 +14,144 @@ set_option old_structure_cmd true
 universe u
 variables {α : Type u}
 
-class weak_order (α : Type u) extends has_le α :=
+class pre_order (α : Type u) extends has_le α, has_lt α :=
 (le_refl : ∀ a : α, a ≤ a)
 (le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
+(lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
+(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a))
+-- TODO(gabriel): default lt_spec to λ a b, iff.refl _
+
+class partial_order (α : Type u) extends pre_order α :=
 (le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)
 
-class linear_weak_order (α : Type u) extends weak_order α :=
+class linear_order (α : Type u) extends partial_order α :=
 (le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)
 
-class strict_order (α : Type u) extends has_lt α :=
-(lt_irrefl : ∀ a : α, ¬ a < a)
-(lt_trans : ∀ a b c : α, a < b → b < c → a < c)
+@[refl] lemma le_refl [pre_order α] : ∀ a : α, a ≤ a :=
+pre_order.le_refl
 
-/- structures with a weak and a strict order -/
-class order_pair (α : Type u) extends weak_order α, has_lt α :=
-(le_of_lt : ∀ a b : α, a < b → a ≤ b)
-(lt_of_lt_of_le : ∀ a b c : α, a < b → b ≤ c → a < c)
-(lt_of_le_of_lt : ∀ a b c : α, a ≤ b → b < c → a < c)
-(lt_irrefl : ∀ a : α, ¬ a < a)
+@[trans] lemma le_trans [pre_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
+pre_order.le_trans
 
-class strong_order_pair (α : Type u) extends weak_order α, has_lt α :=
-(le_iff_lt_or_eq : ∀ a b : α, a ≤ b ↔ a < b ∨ a = b)
-(lt_irrefl : ∀ a : α, ¬ a < a)
+lemma lt_of_le_not_le [pre_order α] : ∀ {a b : α}, a ≤ b → ¬ b ≤ a → a < b
+| a b hab hba := (pre_order.lt_iff_le_not_le _ _).mpr ⟨hab, hba⟩
 
-class linear_order_pair (α : Type u) extends order_pair α, linear_weak_order α
+lemma le_not_le_of_lt [pre_order α] : ∀ {a b : α}, a < b → a ≤ b ∧ ¬ b ≤ a
+| a b hab := (pre_order.lt_iff_le_not_le _ _).mp hab
 
-class linear_strong_order_pair (α : Type u) extends strong_order_pair α, linear_weak_order α
+lemma le_antisymm [partial_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
+partial_order.le_antisymm
 
-@[refl] lemma le_refl [weak_order α] : ∀ a : α, a ≤ a :=
-weak_order.le_refl
-
-@[trans] lemma le_trans [weak_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
-weak_order.le_trans
-
-lemma le_antisymm [weak_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
-weak_order.le_antisymm
-
-lemma le_of_eq [weak_order α] {a b : α} : a = b → a ≤ b :=
+lemma le_of_eq [partial_order α] {a b : α} : a = b → a ≤ b :=
 λ h, h ▸ le_refl a
 
-lemma le_antisymm_iff [weak_order α] {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a :=
+lemma le_antisymm_iff [partial_order α] {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a :=
 ⟨λe, ⟨le_of_eq e, le_of_eq e.symm⟩, λ⟨h1, h2⟩, le_antisymm h1 h2⟩
 
-@[trans] lemma ge_trans [weak_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
+@[trans] lemma ge_trans [pre_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
 λ a b c h₁ h₂, le_trans h₂ h₁
 
-lemma le_total [linear_weak_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a :=
-linear_weak_order.le_total
+lemma le_total [linear_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a :=
+linear_order.le_total
 
-lemma le_of_not_ge [linear_weak_order α] {a b : α} : ¬ a ≥ b → a ≤ b :=
+lemma le_of_not_ge [linear_order α] {a b : α} : ¬ a ≥ b → a ≤ b :=
 or.resolve_left (le_total b a)
 
-lemma le_of_not_le [linear_weak_order α] {a b : α} : ¬ a ≤ b → b ≤ a :=
+lemma le_of_not_le [linear_order α] {a b : α} : ¬ a ≤ b → b ≤ a :=
 or.resolve_left (le_total a b)
 
-lemma lt_irrefl [strict_order α] : ∀ a : α, ¬ a < a :=
-strict_order.lt_irrefl
+lemma lt_irrefl [pre_order α] : ∀ a : α, ¬ a < a
+| a haa := match le_not_le_of_lt haa with
+  | ⟨h1, h2⟩ := false.rec _ (h2 h1)
+  end
 
-lemma gt_irrefl [strict_order α] : ∀ a : α, ¬ a > a :=
+lemma gt_irrefl [pre_order α] : ∀ a : α, ¬ a > a :=
 lt_irrefl
 
-@[trans] lemma lt_trans [strict_order α] : ∀ {a b c : α}, a < b → b < c → a < c :=
-strict_order.lt_trans
+@[trans] lemma lt_trans [pre_order α] : ∀ {a b c : α}, a < b → b < c → a < c
+| a b c hab hbc :=
+  match le_not_le_of_lt hab, le_not_le_of_lt hbc with
+  | ⟨hab, hba⟩, ⟨hbc, hcb⟩ := lt_of_le_not_le (le_trans hab hbc) (λ hca, hcb (le_trans hca hab))
+  end
 
 def lt.trans := @lt_trans
 
-@[trans] lemma gt_trans [strict_order α] : ∀ {a b c : α}, a > b → b > c → a > c :=
+@[trans] lemma gt_trans [pre_order α] : ∀ {a b c : α}, a > b → b > c → a > c :=
 λ a b c h₁ h₂, lt_trans h₂ h₁
 
 def gt.trans := @gt_trans
 
-lemma ne_of_lt [strict_order α] {a b : α} (h : a < b) : a ≠ b :=
+lemma ne_of_lt [pre_order α] {a b : α} (h : a < b) : a ≠ b :=
 λ he, absurd h (he ▸ lt_irrefl a)
 
-lemma ne_of_gt [strict_order α] {a b : α} (h : a > b) : a ≠ b :=
+lemma ne_of_gt [pre_order α] {a b : α} (h : a > b) : a ≠ b :=
 λ he, absurd h (he ▸ lt_irrefl a)
 
-lemma lt_asymm [strict_order α] {a b : α} (h : a < b) : ¬ b < a :=
+lemma lt_asymm [pre_order α] {a b : α} (h : a < b) : ¬ b < a :=
 λ h1 : b < a, lt_irrefl a (lt_trans h h1)
 
-lemma not_lt_of_gt [strict_order α] {a b : α} (h : a > b) : ¬ a < b :=
+lemma not_lt_of_gt [linear_order α] {a b : α} (h : a > b) : ¬ a < b :=
 lt_asymm h
 
-lemma le_of_lt [order_pair α] : ∀ {a b : α}, a < b → a ≤ b :=
-order_pair.le_of_lt
+lemma le_of_lt [pre_order α] : ∀ {a b : α}, a < b → a ≤ b
+| a b hab := (le_not_le_of_lt hab).left
 
-@[trans] lemma lt_of_lt_of_le [order_pair α] : ∀ {a b c : α}, a < b → b ≤ c → a < c :=
-order_pair.lt_of_lt_of_le
+@[trans] lemma lt_of_lt_of_le [pre_order α] : ∀ {a b c : α}, a < b → b ≤ c → a < c
+| a b c hab hbc :=
+  let ⟨hab, hba⟩ := le_not_le_of_lt hab in
+  lt_of_le_not_le (le_trans hab hbc) $ λ hca, hba (le_trans hbc hca)
 
-@[trans] lemma lt_of_le_of_lt [order_pair α] : ∀ {a b c : α}, a ≤ b → b < c → a < c :=
-order_pair.lt_of_le_of_lt
+@[trans] lemma lt_of_le_of_lt [pre_order α] : ∀ {a b c : α}, a ≤ b → b < c → a < c
+| a b c hab hbc :=
+  let ⟨hbc, hcb⟩ := le_not_le_of_lt hbc in
+  lt_of_le_not_le (le_trans hab hbc) $ λ hca, hcb (le_trans hca hab)
 
-@[trans] lemma gt_of_gt_of_ge [order_pair α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c :=
+@[trans] lemma gt_of_gt_of_ge [pre_order α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c :=
 lt_of_le_of_lt h₂ h₁
 
-@[trans] lemma gt_of_ge_of_gt [order_pair α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
+@[trans] lemma gt_of_ge_of_gt [pre_order α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
 lt_of_lt_of_le h₂ h₁
 
-instance order_pair.to_strict_order [s : order_pair α] : strict_order α :=
-{ s with
-  lt_irrefl := order_pair.lt_irrefl,
-  lt_trans  := λ a b c h₁ h₂, lt_of_lt_of_le h₁ (le_of_lt h₂) }
+lemma not_le_of_gt [pre_order α] {a b : α} (h : a > b) : ¬ a ≤ b :=
+(le_not_le_of_lt h).right
 
-lemma not_le_of_gt [order_pair α] {a b : α} (h : a > b) : ¬ a ≤ b :=
-λ h₁, lt_irrefl b (lt_of_lt_of_le h h₁)
+lemma not_lt_of_ge [pre_order α] {a b : α} (h : a ≥ b) : ¬ a < b :=
+λ hab, not_le_of_gt hab h
 
-lemma not_lt_of_ge [order_pair α] {a b : α} (h : a ≥ b) : ¬ a < b :=
-λ h₁, lt_irrefl b (lt_of_le_of_lt h h₁)
+lemma lt_or_eq_of_le [partial_order α] : ∀ {a b : α}, a ≤ b → a < b ∨ a = b
+| a b hab := classical.by_cases
+  (λ hba : b ≤ a, or.inr (le_antisymm hab hba))
+  (λ hba, or.inl (lt_of_le_not_le hab hba))
 
-lemma le_iff_lt_or_eq [strong_order_pair α] : ∀ {a b : α}, a ≤ b ↔ a < b ∨ a = b :=
-strong_order_pair.le_iff_lt_or_eq
+lemma le_of_lt_or_eq [partial_order α] : ∀ {a b : α}, (a < b ∨ a = b) → a ≤ b
+| a b (or.inl hab) := le_of_lt hab
+| a b (or.inr hab) := hab ▸ le_refl _
 
-lemma lt_or_eq_of_le [strong_order_pair α] : ∀ {a b : α}, a ≤ b → a < b ∨ a = b :=
-λ a b h, iff.mp le_iff_lt_or_eq h
+lemma le_iff_lt_or_eq [partial_order α] : ∀ {a b : α}, a ≤ b ↔ a < b ∨ a = b
+| a b := ⟨lt_or_eq_of_le, le_of_lt_or_eq⟩
 
-lemma le_of_lt_or_eq [strong_order_pair α] : ∀ {a b : α}, (a < b ∨ a = b) → a ≤ b :=
-λ a b h, iff.mpr le_iff_lt_or_eq h
-
-lemma lt_of_le_of_ne [strong_order_pair α] {a b : α} : a ≤ b → a ≠ b → a < b :=
+lemma lt_of_le_of_ne [partial_order α] {a b : α} : a ≤ b → a ≠ b → a < b :=
 λ h₁ h₂, or.resolve_right (lt_or_eq_of_le h₁) h₂
 
-private lemma lt_irrefl' [strong_order_pair α] : ∀ a : α, ¬ a < a :=
-strong_order_pair.lt_irrefl
+-- private lemma lt_of_lt_of_le' [strong_order_pair α] (a b c : α) (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
+-- have a ≤ c, from le_trans (le_of_lt' h₁) h₂,
+-- or.elim (lt_or_eq_of_le this)
+--   (λ h : a < c, h)
+--   (λ h : a = c,
+--     have b ≤ a, from h.symm ▸ h₂,
+--     have a = b, from le_antisymm (le_of_lt' h₁) this,
+--     absurd h₁ (this ▸ lt_irrefl' a))
 
-private lemma le_of_lt' [strong_order_pair α] ⦃a b : α⦄ (h : a < b) : a ≤ b :=
-le_of_lt_or_eq (or.inl h)
+-- private lemma lt_of_le_of_lt' [strong_order_pair α] (a b c : α) (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
+-- have a ≤ c, from le_trans h₁ (le_of_lt' h₂),
+-- or.elim (lt_or_eq_of_le this)
+--   (λ h : a < c, h)
+--   (λ h : a = c,
+--     have c ≤ b, from h ▸ h₁,
+--     have c = b, from le_antisymm this (le_of_lt' h₂),
+--     absurd h₂ (this ▸ lt_irrefl' c))
 
-private lemma lt_of_lt_of_le' [strong_order_pair α] (a b c : α) (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
-have a ≤ c, from le_trans (le_of_lt' h₁) h₂,
-or.elim (lt_or_eq_of_le this)
-  (λ h : a < c, h)
-  (λ h : a = c,
-    have b ≤ a, from h.symm ▸ h₂,
-    have a = b, from le_antisymm (le_of_lt' h₁) this,
-    absurd h₁ (this ▸ lt_irrefl' a))
-
-private lemma lt_of_le_of_lt' [strong_order_pair α] (a b c : α) (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
-have a ≤ c, from le_trans h₁ (le_of_lt' h₂),
-or.elim (lt_or_eq_of_le this)
-  (λ h : a < c, h)
-  (λ h : a = c,
-    have c ≤ b, from h ▸ h₁,
-    have c = b, from le_antisymm this (le_of_lt' h₂),
-    absurd h₂ (this ▸ lt_irrefl' c))
-
-instance strong_order_pair.to_order_pair [s : strong_order_pair α] : order_pair α :=
-{ s with
-  lt_irrefl      := lt_irrefl',
-  le_of_lt       := le_of_lt',
-  lt_of_le_of_lt := lt_of_le_of_lt',
-  lt_of_lt_of_le := lt_of_lt_of_le'}
-
-instance linear_strong_order_pair.to_linear_order_pair [s : linear_strong_order_pair α] : linear_order_pair α :=
-{ s with
-  lt_irrefl      := lt_irrefl',
-  le_of_lt       := le_of_lt',
-  lt_of_le_of_lt := lt_of_le_of_lt',
-  lt_of_lt_of_le := lt_of_lt_of_le'}
-
-lemma lt_trichotomy [linear_strong_order_pair α] (a b : α) : a < b ∨ a = b ∨ b < a :=
+lemma lt_trichotomy [linear_order α] (a b : α) : a < b ∨ a = b ∨ b < a :=
 or.elim (le_total a b)
   (λ h : a ≤ b, or.elim (lt_or_eq_of_le h)
     (λ h : a < b, or.inl h)
@@ -181,67 +160,72 @@ or.elim (le_total a b)
     (λ h : b < a, or.inr (or.inr h))
     (λ h : b = a, or.inr (or.inl h.symm)))
 
-
-lemma le_of_not_gt [linear_strong_order_pair α] {a b : α} (h : ¬ a > b) : a ≤ b :=
+lemma le_of_not_gt [linear_order α] {a b : α} (h : ¬ a > b) : a ≤ b :=
 match lt_trichotomy a b with
 | or.inl hlt          := le_of_lt hlt
 | or.inr (or.inl heq) := heq ▸ le_refl a
 | or.inr (or.inr hgt) := absurd hgt h
 end
 
-lemma lt_of_not_ge [linear_strong_order_pair α] {a b : α} (h : ¬ a ≥ b) : a < b :=
+lemma lt_of_not_ge [linear_order α] {a b : α} (h : ¬ a ≥ b) : a < b :=
 match lt_trichotomy a b with
 | or.inl hlt          := hlt
 | or.inr (or.inl heq) := absurd (heq ▸ le_refl a : a ≥ b) h
 | or.inr (or.inr hgt) := absurd (le_of_lt hgt) h
 end
 
-lemma lt_or_ge [linear_strong_order_pair α] (a b : α) : a < b ∨ a ≥ b :=
+lemma lt_or_ge [linear_order α] (a b : α) : a < b ∨ a ≥ b :=
 match lt_trichotomy a b with
 | or.inl hlt          := or.inl hlt
 | or.inr (or.inl heq) := or.inr (heq ▸ le_refl a)
 | or.inr (or.inr hgt) := or.inr (le_of_lt hgt)
 end
 
-lemma le_or_gt [linear_strong_order_pair α] (a b : α) : a ≤ b ∨ a > b :=
+lemma le_or_gt [linear_order α] (a b : α) : a ≤ b ∨ a > b :=
 or.swap (lt_or_ge b a)
 
-lemma lt_or_gt_of_ne [linear_strong_order_pair α] {a b : α} (h : a ≠ b) : a < b ∨ a > b :=
+lemma lt_or_gt_of_ne [linear_order α] {a b : α} (h : a ≠ b) : a < b ∨ a > b :=
 match lt_trichotomy a b with
 | or.inl hlt          := or.inl hlt
 | or.inr (or.inl heq) := absurd heq h
 | or.inr (or.inr hgt) := or.inr hgt
 end
 
-lemma ne_iff_lt_or_gt [linear_strong_order_pair α] {a b : α} : a ≠ b ↔ a < b ∨ a > b :=
+lemma ne_iff_lt_or_gt [linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ a > b :=
 ⟨lt_or_gt_of_ne, λo, or.elim o ne_of_lt ne_of_gt⟩
 
-lemma lt_iff_not_ge [linear_strong_order_pair α] (x y : α) : x < y ↔ ¬ x ≥ y :=
+lemma lt_iff_not_ge [linear_order α] (x y : α) : x < y ↔ ¬ x ≥ y :=
 ⟨not_le_of_gt, lt_of_not_ge⟩
 
-/- The following lemma can be used when defining a decidable_linear_order instance, and the concrete structure
-   does not have its own definition for decidable le  -/
-def decidable_le_of_decidable_lt [linear_strong_order_pair α] [∀ a b : α, decidable (a < b)] (a b : α) : decidable (a ≤ b) :=
-if h₁ : a < b      then is_true (le_of_lt h₁)
-else if h₂ : b < a then is_false (not_le_of_gt h₂)
-else                    is_true (le_of_not_gt h₂)
+instance decidable_lt_of_decidable_le [pre_order α]
+  [decidable_rel ((≤) : α → α → Prop)] :
+  decidable_rel ((<) : α → α → Prop)
+| a b :=
+  if hab : a ≤ b then
+    if hba : b ≤ a then
+      is_false $ λ hab', not_le_of_gt hab' hba
+    else
+      is_true $ lt_of_le_not_le hab hba
+  else
+    is_false $ λ hab', hab (le_of_lt hab')
 
-/- The following lemma can be used when defining a decidable_linear_order instance, and the concrete structure
-   does not have its own definition for decidable le -/
-def decidable_eq_of_decidable_lt [linear_strong_order_pair α] [∀ a b : α, decidable (a < b)] (a b : α) : decidable (a = b) :=
-match decidable_le_of_decidable_lt a b with
-| is_true h₁  :=
-  match decidable_le_of_decidable_lt b a with
-  | is_true h₂  := is_true (le_antisymm h₁ h₂)
-  | is_false h₂ := is_false (λ he : a = b, h₂ (he ▸ le_refl a))
-  end
-| is_false h₁ := is_false (λ he : a = b, h₁ (he ▸ le_refl a))
-end
+instance decidable_eq_of_decidable_le [partial_order α]
+  [decidable_rel ((≤) : α → α → Prop)] :
+  decidable_eq α
+| a b :=
+  if hab : a ≤ b then
+    if hba : b ≤ a then
+      is_true (le_antisymm hab hba)
+    else
+      is_false (λ heq, hba (heq ▸ le_refl _))
+  else
+    is_false (λ heq, hab (heq ▸ le_refl _))
 
-class decidable_linear_order (α : Type u) extends linear_strong_order_pair α :=
-(decidable_lt : decidable_rel lt)
-(decidable_le : decidable_rel le) -- TODO(Leo): add default value using decidable_le_of_decidable_lt
-(decidable_eq : decidable_eq α)   -- TODO(Leo): add default value using decidable_eq_of_decidable_lt
+-- TODO(leo,gabriel): add default values
+class decidable_linear_order (α : Type u) extends linear_order α :=
+(decidable_le : decidable_rel le)
+(decidable_eq : decidable_eq α)
+(decidable_lt : decidable_rel ((<) : α → α → Prop))
 
 instance [decidable_linear_order α] (a b : α) : decidable (a < b) :=
 decidable_linear_order.decidable_lt α a b
diff --git a/library/init/algebra/ordered_group.lean b/library/init/algebra/ordered_group.lean
index 343ba77136..fe53d1f5ae 100644
--- a/library/init/algebra/ordered_group.lean
+++ b/library/init/algebra/ordered_group.lean
@@ -16,7 +16,7 @@ universe u
 
 class ordered_cancel_comm_monoid (α : Type u)
       extends add_comm_monoid α, add_left_cancel_semigroup α,
-              add_right_cancel_semigroup α, order_pair α :=
+              add_right_cancel_semigroup α, partial_order α :=
 (add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
 (le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c)
 (add_lt_add_left       : ∀ a b : α, a < b → ∀ c : α, c + a < c + b)
@@ -183,7 +183,7 @@ add_zero c ▸ add_lt_add hbc ha
 
 end ordered_cancel_comm_monoid
 
-class ordered_comm_group (α : Type u) extends add_comm_group α, order_pair α :=
+class ordered_comm_group (α : Type u) extends add_comm_group α, partial_order α :=
 (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
 (add_lt_add_left : ∀ a b : α, a < b → ∀ c : α, c + a < c + b)
 
@@ -615,10 +615,7 @@ class decidable_linear_ordered_comm_group (α : Type u)
 
 instance decidable_linear_ordered_comm_group.to_ordered_comm_group (α : Type u)
   [s : decidable_linear_ordered_comm_group α] : ordered_comm_group α :=
-{s with
- le_of_lt := @le_of_lt α _,
- lt_of_le_of_lt := @lt_of_le_of_lt α _,
- lt_of_lt_of_le := @lt_of_lt_of_le α _ }
+{ s with add := s.add }
 
 class decidable_linear_ordered_cancel_comm_monoid (α : Type u)
       extends ordered_cancel_comm_monoid α, decidable_linear_order α
diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean
index 727c2b9e5a..1e2cb09c2e 100644
--- a/library/init/algebra/ordered_ring.lean
+++ b/library/init/algebra/ordered_ring.lean
@@ -86,7 +86,7 @@ lemma mul_self_lt_mul_self {a b : α} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b *
 mul_lt_mul' (le_of_lt h2) h2 h1 (lt_of_le_of_lt h1 h2)
 end ordered_semiring
 
-class linear_ordered_semiring (α : Type u) extends ordered_semiring α, linear_strong_order_pair α :=
+class linear_ordered_semiring (α : Type u) extends ordered_semiring α, linear_order α :=
 (zero_lt_one : zero < one)
 
 section linear_ordered_semiring
@@ -258,8 +258,8 @@ by rwa zero_mul at this
 
 end ordered_ring
 
-class linear_ordered_ring (α : Type u) extends ordered_ring α, linear_strong_order_pair α :=
-(zero_lt_one : lt zero one)
+class linear_ordered_ring (α : Type u) extends ordered_ring α, linear_order α :=
+(zero_lt_one : zero < one)
 
 instance linear_ordered_ring.to_linear_ordered_semiring [s : linear_ordered_ring α] : linear_ordered_semiring α :=
 { s with
diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean
index 4fcad5b7cb..8d80390dca 100644
--- a/library/init/data/int/order.lean
+++ b/library/init/data/int/order.lean
@@ -207,6 +207,13 @@ iff.mpr
   (int.lt_iff_le_and_ne _ _)
   (and.intro hac (assume heq, int.not_le_of_gt begin rw heq, exact hbc end hab))
 
+protected lemma lt_iff_le_not_le {a b : ℤ} : a < b ↔ (a ≤ b ∧ ¬ b ≤ a) :=
+begin
+simp [int.lt_iff_le_and_ne], split; intro h; cases h with hneq hab; split,
+{assumption}, {intro hba, apply hneq, apply int.le_antisymm; assumption},
+{intro heq, apply hab, subst heq, apply int.le_refl}, {assumption}
+end
+
 instance : decidable_linear_ordered_comm_ring int :=
 { int.comm_ring with
   le              := int.le,
@@ -214,16 +221,12 @@ instance : decidable_linear_ordered_comm_ring int :=
   le_trans        := @int.le_trans,
   le_antisymm     := @int.le_antisymm,
   lt              := int.lt,
-  le_of_lt        := @int.le_of_lt,
-  lt_of_lt_of_le  := @int.lt_of_lt_of_le,
-  lt_of_le_of_lt  := @int.lt_of_le_of_lt,
-  lt_irrefl       := int.lt_irrefl,
+  lt_iff_le_not_le := @int.lt_iff_le_not_le,
   add_le_add_left := @int.add_le_add_left,
   add_lt_add_left := @int.add_lt_add_left,
   zero_ne_one     := zero_ne_one,
   mul_nonneg      := @int.mul_nonneg,
   mul_pos         := @int.mul_pos,
-  le_iff_lt_or_eq := int.le_iff_lt_or_eq,
   le_total        := int.le_total,
   zero_lt_one     := int.zero_lt_one,
   decidable_eq    := int.decidable_eq,
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index 5d66a04792..254a733037 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -187,8 +187,36 @@ lemma lt_succ_self (n : ℕ) : n < succ n := lt.base n
 protected lemma le_antisymm {n m : ℕ} (h₁ : n ≤ m) : m ≤ n → n = m :=
 less_than_or_equal.cases_on h₁ (λ a, rfl) (λ a b c, absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n))
 
-instance : weak_order ℕ :=
-⟨@nat.less_than_or_equal, @nat.le_refl, @nat.le_trans, @nat.le_antisymm⟩
+protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b
+| a 0     := or.inr (zero_le a)
+| a (b+1) :=
+  match lt_or_ge a b with
+  | or.inl h := or.inl (le_succ_of_le h)
+  | or.inr h :=
+    match nat.eq_or_lt_of_le h with
+    | or.inl h1 := or.inl (h1 ▸ lt_succ_self b)
+    | or.inr h1 := or.inr h1
+    end
+  end
+
+protected lemma le_total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
+or.imp_left nat.le_of_lt (nat.lt_or_ge m n)
+
+protected lemma lt_of_le_and_ne {m n : ℕ} (h1 : m ≤ n) : m ≠ n → m < n :=
+or.resolve_right (or.swap (nat.eq_or_lt_of_le h1))
+
+protected lemma lt_iff_le_not_le {m n : ℕ} : m < n ↔ (m ≤ n ∧ ¬ n ≤ m) :=
+⟨λ hmn, ⟨nat.le_of_lt hmn, λ hnm, nat.lt_irrefl _ (nat.lt_of_le_of_lt hnm hmn)⟩,
+ λ ⟨hmn, hnm⟩, nat.lt_of_le_and_ne hmn (λ heq, hnm (heq ▸ nat.le_refl _))⟩
+
+instance : linear_order ℕ :=
+{ le := nat.less_than_or_equal,
+  le_refl := @nat.le_refl,
+  le_trans := @nat.le_trans,
+  le_antisymm := @nat.le_antisymm,
+  le_total := @nat.le_total,
+  lt := nat.lt,
+  lt_iff_le_not_le := @nat.lt_iff_le_not_le }
 
 lemma eq_zero_of_le_zero {n : nat} (h : n ≤ 0) : n = 0 :=
 le_antisymm h (zero_le _)
@@ -210,18 +238,6 @@ lemma pred_lt_pred : ∀ {n m : ℕ}, n ≠ 0 → m ≠ 0 → n < m → pred n <
 | _         0       h₁ h₂ h := absurd rfl h₂
 | (succ n) (succ m) _  _  h := lt_of_succ_lt_succ h
 
-protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b
-| a 0     := or.inr (zero_le a)
-| a (b+1) :=
-  match lt_or_ge a b with
-  | or.inl h := or.inl (le_succ_of_le h)
-  | or.inr h :=
-    match nat.eq_or_lt_of_le h with
-    | or.inl h1 := or.inl (h1 ▸ lt_succ_self b)
-    | or.inr h1 := or.inr h1
-    end
-  end
-
 lemma lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h
 
 lemma succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h
@@ -270,9 +286,6 @@ end
 protected lemma add_le_add_iff_le_right (k n m : ℕ) : n + k ≤ m + k ↔ n ≤ m :=
   ⟨ nat.le_of_add_le_add_right , assume h, nat.add_le_add_right h _ ⟩
 
-protected lemma lt_of_le_and_ne {m n : ℕ} (h1 : m ≤ n) : m ≠ n → m < n :=
-or.resolve_right (or.swap (nat.eq_or_lt_of_le h1))
-
 protected theorem lt_of_add_lt_add_left {k n m : ℕ} (h : k + n < k + m) : n < m :=
 let h' := nat.le_of_lt h in
 nat.lt_of_le_and_ne
@@ -294,9 +307,6 @@ by rw add_comm; exact nat.lt_add_of_pos_right h
 protected lemma zero_lt_one : 0 < (1:nat) :=
 zero_lt_succ 0
 
-protected lemma le_total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
-or.imp_left nat.le_of_lt (nat.lt_or_ge m n)
-
 protected lemma le_of_lt_or_eq {m n : ℕ} (h : m < n ∨ m = n) : m ≤ n :=
 nat.le_of_eq_or_lt (or.swap h)
 
@@ -332,12 +342,8 @@ instance : decidable_linear_ordered_semiring nat :=
   le_trans                   := @nat.le_trans,
   le_antisymm                := @nat.le_antisymm,
   le_total                   := @nat.le_total,
-  le_iff_lt_or_eq            := @nat.le_iff_lt_or_eq,
-  le_of_lt                   := @nat.le_of_lt,
-  lt_irrefl                  := @nat.lt_irrefl,
-  lt_of_lt_of_le             := @nat.lt_of_lt_of_le,
-  lt_of_le_of_lt             := @nat.lt_of_le_of_lt,
   lt_of_add_lt_add_left      := @nat.lt_of_add_lt_add_left,
+  lt_iff_le_not_le           := pre_order.lt_iff_le_not_le,
   add_lt_add_left            := @nat.add_lt_add_left,
   add_le_add_left            := @nat.add_le_add_left,
   le_of_add_le_add_left      := @nat.le_of_add_le_add_left,
diff --git a/src/library/arith_instance.cpp b/src/library/arith_instance.cpp
index eaff0b026d..ad13c90731 100644
--- a/src/library/arith_instance.cpp
+++ b/src/library/arith_instance.cpp
@@ -75,7 +75,7 @@ expr arith_instance::mk_le() { return mk_op(get_has_le_le_name(), get_has_le_nam
 
 expr arith_instance::mk_bit0() { return mk_op(get_bit0_name(), get_has_add_name(), m_info->m_bit0); }
 
-expr arith_instance::mk_weark_order() { return mk_structure(get_weak_order_name(), m_info->m_weak_order); }
+expr arith_instance::mk_partial_order() { return mk_structure(get_partial_order_name(), m_info->m_partial_order); }
 expr arith_instance::mk_add_comm_semigroup() { return mk_structure(get_add_comm_semigroup_name(), m_info->m_add_comm_semigroup); }
 expr arith_instance::mk_monoid() { return mk_structure(get_monoid_name(), m_info->m_monoid); }
 expr arith_instance::mk_add_monoid() { return mk_structure(get_add_monoid_name(), m_info->m_add_monoid); }
diff --git a/src/library/arith_instance.h b/src/library/arith_instance.h
index 2c93d079fa..0b901d902f 100644
--- a/src/library/arith_instance.h
+++ b/src/library/arith_instance.h
@@ -22,7 +22,7 @@ class arith_instance_info {
     optional<expr> m_bit0, m_bit1;
 
     /* Structures */
-    optional<expr> m_weak_order;
+    optional<expr> m_partial_order;
     optional<expr> m_add_comm_semigroup;
     optional<expr> m_monoid, m_add_monoid;
     optional<expr> m_add_group, m_add_comm_group;
@@ -86,7 +86,7 @@ public:
     expr mk_has_lt() { return app_arg(mk_lt()); }
     expr mk_has_le() { return app_arg(mk_le()); }
 
-    expr mk_weark_order();
+    expr mk_partial_order();
     expr mk_add_comm_semigroup();
     expr mk_monoid();
     expr mk_add_monoid();
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 592fc2794b..759c0a3441 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -368,7 +368,7 @@ name const * g_unit_star = nullptr;
 name const * g_unsafe_monad_from_pure_bind = nullptr;
 name const * g_user_attribute = nullptr;
 name const * g_vm_monitor = nullptr;
-name const * g_weak_order = nullptr;
+name const * g_partial_order = nullptr;
 name const * g_well_founded_fix = nullptr;
 name const * g_well_founded_fix_eq = nullptr;
 name const * g_well_founded_tactics = nullptr;
@@ -745,7 +745,7 @@ void initialize_constants() {
     g_unsafe_monad_from_pure_bind = new name{"unsafe_monad_from_pure_bind"};
     g_user_attribute = new name{"user_attribute"};
     g_vm_monitor = new name{"vm_monitor"};
-    g_weak_order = new name{"weak_order"};
+    g_partial_order = new name{"partial_order"};
     g_well_founded_fix = new name{"well_founded", "fix"};
     g_well_founded_fix_eq = new name{"well_founded", "fix_eq"};
     g_well_founded_tactics = new name{"well_founded_tactics"};
@@ -1123,7 +1123,7 @@ void finalize_constants() {
     delete g_unsafe_monad_from_pure_bind;
     delete g_user_attribute;
     delete g_vm_monitor;
-    delete g_weak_order;
+    delete g_partial_order;
     delete g_well_founded_fix;
     delete g_well_founded_fix_eq;
     delete g_well_founded_tactics;
@@ -1500,7 +1500,7 @@ name const & get_unit_star_name() { return *g_unit_star; }
 name const & get_unsafe_monad_from_pure_bind_name() { return *g_unsafe_monad_from_pure_bind; }
 name const & get_user_attribute_name() { return *g_user_attribute; }
 name const & get_vm_monitor_name() { return *g_vm_monitor; }
-name const & get_weak_order_name() { return *g_weak_order; }
+name const & get_partial_order_name() { return *g_partial_order; }
 name const & get_well_founded_fix_name() { return *g_well_founded_fix; }
 name const & get_well_founded_fix_eq_name() { return *g_well_founded_fix_eq; }
 name const & get_well_founded_tactics_name() { return *g_well_founded_tactics; }
diff --git a/src/library/constants.h b/src/library/constants.h
index cbd9cf9f29..52755138fd 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -370,7 +370,7 @@ name const & get_unit_star_name();
 name const & get_unsafe_monad_from_pure_bind_name();
 name const & get_user_attribute_name();
 name const & get_vm_monitor_name();
-name const & get_weak_order_name();
+name const & get_partial_order_name();
 name const & get_well_founded_fix_name();
 name const & get_well_founded_fix_eq_name();
 name const & get_well_founded_tactics_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 46a86c808e..2fa0ebd2e5 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -363,7 +363,7 @@ unit.star
 unsafe_monad_from_pure_bind
 user_attribute
 vm_monitor
-weak_order
+partial_order
 well_founded.fix
 well_founded.fix_eq
 well_founded_tactics
diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp
index 3fedbf9502..1dcdab748e 100644
--- a/src/library/norm_num.cpp
+++ b/src/library/norm_num.cpp
@@ -371,7 +371,7 @@ expr norm_num_context::mk_nonneg_prf(expr const & e) {
     } else if (is_one(e)) {
         return mk_app({mk_const(get_zero_le_one_name()), type, mk_lin_ord_semiring()});
     } else if (is_zero(e)) {
-        return mk_app({mk_const(get_le_refl_name()), type, mk_wk_order(), mk_zero()});
+        return mk_app({mk_const(get_le_refl_name()), type, mk_partial_order(), mk_zero()});
     } else {
         throw exception("mk_nonneg_proof called on zero or non_numeral");
     }
diff --git a/src/library/norm_num.h b/src/library/norm_num.h
index 883893aa78..1a76a438cf 100644
--- a/src/library/norm_num.h
+++ b/src/library/norm_num.h
@@ -52,7 +52,7 @@ class norm_num_context {
     expr mk_field() { return m_ainst.mk_field(); }
     expr mk_lin_ord_semiring() { return m_ainst.mk_linear_ordered_semiring(); }
     expr mk_lin_ord_ring() { return m_ainst.mk_linear_ordered_ring(); }
-    expr mk_wk_order() { return m_ainst.mk_weark_order(); }
+    expr mk_partial_order() { return m_ainst.mk_partial_order(); }
 
     expr mk_num(mpq const & q) { return m_ainst.mk_num(q); }
 
diff --git a/tests/lean/apply_tac.lean b/tests/lean/apply_tac.lean
index bf1a7c738d..e93bb5a0e6 100644
--- a/tests/lean/apply_tac.lean
+++ b/tests/lean/apply_tac.lean
@@ -32,7 +32,7 @@ begin
   refl
 end
 
-example {α : Type} [weak_order α] (a : α) : a = a :=
+example {α : Type} [partial_order α] (a : α) : a = a :=
 begin
   apply le_antisymm,
   apply le_refl,
diff --git a/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out b/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out
index 4a93be4e8b..b510676290 100644
--- a/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out
+++ b/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out
@@ -1,11 +1,11 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"message":"file invalidated","response":"ok","seq_num":1}
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\ntermhas type\n  Type"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\ntermhas type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\ntermhas type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\nterm has type\n  Type"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\nterm has type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\nterm has type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":2}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\ntermhas type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\nterm has type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
 {"msgs":[],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"}],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"},{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean
index 846a49085b..e2272eead6 100644
--- a/tests/lean/run/check_constants.lean
+++ b/tests/lean/run/check_constants.lean
@@ -368,7 +368,7 @@ run_cmd script_check_id `unit.star
 run_cmd script_check_id `unsafe_monad_from_pure_bind
 run_cmd script_check_id `user_attribute
 run_cmd script_check_id `vm_monitor
-run_cmd script_check_id `weak_order
+run_cmd script_check_id `partial_order
 run_cmd script_check_id `well_founded.fix
 run_cmd script_check_id `well_founded.fix_eq
 run_cmd script_check_id `well_founded_tactics