diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 25e4993ce..5e3c05194 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -45,22 +45,22 @@ notation a >= b := has_le.ge a b
 definition has_lt.gt {A : Type} [s : has_lt A] (a b : A) := b < a
 notation a > b := has_lt.gt a b
 
-theorem eq_le_trans {A : Type} [s : has_le A] {a b c : A} (H1 : a = b) (H2 : b ≤ c) :
+theorem le_of_eq_of_le {A : Type} [s : has_le A] {a b c : A} (H1 : a = b) (H2 : b ≤ c) :
   a ≤ c := H1⁻¹ ▸ H2
 
-theorem le_eq_trans {A : Type} [s : has_le A] {a b c : A} (H1 : a ≤ b) (H2 : b = c) :
+theorem le_of_le_of_eq {A : Type} [s : has_le A] {a b c : A} (H1 : a ≤ b) (H2 : b = c) :
   a ≤ c := H2 ▸ H1
 
-theorem eq_lt_trans {A : Type} [s : has_lt A] {a b c : A} (H1 : a = b) (H2 : b < c) :
+theorem lt_of_eq_of_lt {A : Type} [s : has_lt A] {a b c : A} (H1 : a = b) (H2 : b < c) :
   a < c := H1⁻¹ ▸ H2
 
-theorem lt_eq_trans {A : Type} [s : has_lt A] {a b c : A} (H1 : a < b) (H2 : b = c) :
+theorem lt_of_lt_of_eq {A : Type} [s : has_lt A] {a b c : A} (H1 : a < b) (H2 : b = c) :
   a < c := H2 ▸ H1
 
-calc_trans eq_le_trans
-calc_trans le_eq_trans
-calc_trans eq_lt_trans
-calc_trans lt_eq_trans
+calc_trans le_of_eq_of_le
+calc_trans le_of_le_of_eq
+calc_trans lt_of_eq_of_lt
+calc_trans lt_of_lt_of_eq
 
 
 /- weak orders -/
@@ -70,18 +70,18 @@ structure weak_order [class] (A : Type) extends has_le A :=
 (le_trans : ∀a b c, le a b → le b c → le a c)
 (le_antisym : ∀a b, le a b → le b a → a = b)
 
-theorem le_refl [s : weak_order A] (a : A) : a ≤ a := !weak_order.le_refl
+theorem le.refl [s : weak_order A] (a : A) : a ≤ a := !weak_order.le_refl
 
-theorem le_trans [s : weak_order A] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
+theorem le.trans [s : weak_order A] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
 
-calc_trans le_trans
+calc_trans le.trans
 
-theorem le_antisym [s : weak_order A] {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisym
+theorem le.antisym [s : weak_order A] {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisym
 
 structure linear_weak_order [class] (A : Type) extends weak_order A :=
 (le_total : ∀a b, le a b ∨ le b a)
 
-theorem le_total [s : linear_weak_order A] {a b : A} : a ≤ b ∨ b ≤ a :=
+theorem le.total [s : linear_weak_order A] {a b : A} : a ≤ b ∨ b ≤ a :=
 !linear_weak_order.le_total
 
 
@@ -91,28 +91,30 @@ structure strict_order [class] (A : Type) extends has_lt A :=
 (lt_irrefl : ∀a, ¬ lt a a)
 (lt_trans : ∀a b c, lt a b → lt b c → lt a c)
 
-theorem lt_irrefl [s : strict_order A] (a : A) : ¬ a < a := !strict_order.lt_irrefl
+theorem lt.irrefl [s : strict_order A] (a : A) : ¬ a < a := !strict_order.lt_irrefl
 
-theorem lt_trans [s : strict_order A] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
+theorem lt.trans [s : strict_order A] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
 
-calc_trans lt_trans
+calc_trans lt.trans
 
-theorem lt_imp_ne [s : strict_order A] {a b : A} : a < b → a ≠ b :=
-assume lt_ab : a < b, assume eq_ab : a = b, lt_irrefl a (eq_ab⁻¹ ▸ lt_ab)
+theorem lt.ne [s : strict_order A] {a b : A} : a < b → a ≠ b :=
+assume lt_ab : a < b, assume eq_ab : a = b, lt.irrefl a (eq_ab⁻¹ ▸ lt_ab)
 
 
 /- well-founded orders -/
 
+-- TODO: do these duplicate what Leo has done? if so, eliminate
+
 structure wf_strict_order [class] (A : Type) extends strict_order A :=
 (wf_rec : ∀P : A → Type, (∀x, (∀y, lt y x → P y) → P x) → ∀x, P x)
 
-definition wf_rec_on {A : Type} [s : wf_strict_order A] {P : A → Type}
+definition wf.rec_on {A : Type} [s : wf_strict_order A] {P : A → Type}
     (x : A) (H : ∀x, (∀y, wf_strict_order.lt y x → P y) → P x) : P x :=
 wf_strict_order.wf_rec P H x
 
-theorem wf_ind_on.{u v} {A : Type.{u}} [s : wf_strict_order.{u 0} A] {P : A → Prop}
+theorem wf.ind_on.{u v} {A : Type.{u}} [s : wf_strict_order.{u 0} A] {P : A → Prop}
     (x : A) (H : ∀x, (∀y, wf_strict_order.lt y x → P y) → P x) : P x :=
-wf_rec_on x H
+wf.rec_on x H
 
 
 /- structures with a weak and a strict order -/
@@ -120,14 +122,14 @@ wf_rec_on x H
 structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
 (lt_iff_le_ne : ∀a b, lt a b ↔ (le a b ∧ a ≠ b))
 
-theorem lt_iff_le_ne [s : order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) :=
+theorem lt_iff_le_and_ne [s : order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) :=
 !order_pair.lt_iff_le_ne
 
-theorem lt_imp_le [s : order_pair A] {a b : A} (H : a < b) : a ≤ b :=
-and.elim_left (iff.mp lt_iff_le_ne H)
+theorem le_of_lt [s : order_pair A] {a b : A} (H : a < b) : a ≤ b :=
+and.elim_left (iff.mp lt_iff_le_and_ne H)
 
-theorem le_ne_imp_lt [s : order_pair A] {a b : A} (H1 : a ≤ b) (H2 : a ≠ b) : a < b :=
-iff.mp (iff.symm lt_iff_le_ne) (and.intro H1 H2)
+theorem lt_of_le_of_ne [s : order_pair A] {a b : A} (H1 : a ≤ b) (H2 : a ≠ b) : a < b :=
+iff.mp (iff.symm lt_iff_le_and_ne) (and.intro H1 H2)
 
 definition order_pair.to_strict_order [instance] [s : order_pair A] : strict_order A :=
 strict_order.mk
@@ -135,49 +137,49 @@ strict_order.mk
   (show ∀a, ¬ a < a, from
     take a,
     assume H : a < a,
-    have H1 : a ≠ a, from and.elim_right (iff.mp !lt_iff_le_ne H),
+    have H1 : a ≠ a, from and.elim_right (iff.mp !lt_iff_le_and_ne H),
     H1 rfl)
   (show ∀a b c, a < b → b < c → a < c, from
     take a b c,
     assume lt_ab : a < b,
-    have le_ab : a ≤ b, from lt_imp_le lt_ab,
+    have le_ab : a ≤ b, from le_of_lt lt_ab,
     assume lt_bc : b < c,
-    have le_bc : b ≤ c, from lt_imp_le lt_bc,
-    have le_ac : a ≤ c, from le_trans le_ab le_bc,
+    have le_bc : b ≤ c, from le_of_lt lt_bc,
+    have le_ac : a ≤ c, from le.trans le_ab le_bc,
     have ne_ac : a ≠ c, from
       assume eq_ac : a = c,
       have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
-      have eq_ab : a = b, from le_antisym le_ab le_ba,
-      have ne_ab : a ≠ b, from and.elim_right (iff.mp lt_iff_le_ne lt_ab),
+      have eq_ab : a = b, from le.antisym le_ab le_ba,
+      have ne_ab : a ≠ b, from and.elim_right (iff.mp lt_iff_le_and_ne lt_ab),
       ne_ab eq_ab,
-    show a < c, from le_ne_imp_lt le_ac ne_ac)
+    show a < c, from lt_of_le_of_ne le_ac ne_ac)
 
-theorem lt_le_trans [s : order_pair A] {a b c : A} : a < b → b ≤ c → a < c :=
+theorem lt_of_lt_of_le [s : order_pair A] {a b c : A} : a < b → b ≤ c → a < c :=
 assume lt_ab : a < b,
 assume le_bc : b ≤ c,
-have le_ac : a ≤ c, from le_trans (lt_imp_le lt_ab) le_bc,
+have le_ac : a ≤ c, from le.trans (le_of_lt lt_ab) le_bc,
 have ne_ac : a ≠ c, from
   assume eq_ac : a = c,
   have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
-  have eq_ab : a = b, from le_antisym (lt_imp_le lt_ab) le_ba,
-  show false, from lt_imp_ne lt_ab eq_ab,
-show a < c, from le_ne_imp_lt le_ac ne_ac
+  have eq_ab : a = b, from le.antisym (le_of_lt lt_ab) le_ba,
+  show false, from lt.ne lt_ab eq_ab,
+show a < c, from lt_of_le_of_ne le_ac ne_ac
 
-theorem le_lt_trans [s : order_pair A] {a b c : A} : a ≤ b → b < c → a < c :=
+theorem lt_of_le_of_lt [s : order_pair A] {a b c : A} : a ≤ b → b < c → a < c :=
 assume le_ab : a ≤ b,
 assume lt_bc : b < c,
-have le_ac : a ≤ c, from le_trans le_ab (lt_imp_le lt_bc),
+have le_ac : a ≤ c, from le.trans le_ab (le_of_lt lt_bc),
 have ne_ac : a ≠ c, from
   assume eq_ac : a = c,
   have le_cb : c ≤ b, from eq_ac ▸ le_ab,
-  have eq_bc : b = c, from le_antisym (lt_imp_le lt_bc) le_cb,
-  show false, from lt_imp_ne lt_bc eq_bc,
-show a < c, from le_ne_imp_lt le_ac ne_ac
+  have eq_bc : b = c, from le.antisym (le_of_lt lt_bc) le_cb,
+  show false, from lt.ne lt_bc eq_bc,
+show a < c, from lt_of_le_of_ne le_ac ne_ac
 
-calc_trans le_lt_trans
-calc_trans lt_le_trans
+calc_trans lt_of_lt_of_le
+calc_trans lt_of_le_of_lt
 
-structure strong_order_pair [class] (A : Type) extends strict_order A, has_le A :=
+structure strong_order_pair [class] (A : Type) extends order_pair A :=
 (le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
 
 theorem le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ∨ a = b :=
@@ -186,19 +188,24 @@ theorem le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b
 theorem le_imp_lt_or_eq [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ∨ a = b :=
 iff.mp le_iff_lt_or_eq le_ab
 
-definition strong_order_pair.to_order_pair [instance] [s : strong_order_pair A] : order_pair A :=
-order_pair.mk
-  strong_order_pair.le
-  (take a, show a ≤ a, from iff.mp (iff.symm le_iff_lt_or_eq) (or.intro_right _ rfl))
+-- We can also construct a strong order pair by defining a strict order, and then defining
+-- x ≤ y ↔ x < y ∨ x = y
+
+structure strict_order_with_le [class] (A : Type) extends strict_order A, has_le A :=
+(le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
+
+definition strict_order_with_le.to_order_pair [instance] [s : strict_order_with_le A] : strong_order_pair A :=
+strong_order_pair.mk strict_order_with_le.le
+  (take a, show a ≤ a, from iff.mp (iff.symm !strict_order_with_le.le_iff_lt_or_eq) (or.intro_right _ rfl))
   (take a b c,
     assume le_ab : a ≤ b,
     assume le_bc : b ≤ c,
     show a ≤ c, from
-      or.elim (le_imp_lt_or_eq le_ab)
+      or.elim (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ab)
         (assume lt_ab : a < b,
-          or.elim (le_imp_lt_or_eq le_bc)
+          or.elim (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_bc)
             (assume lt_bc : b < c,
-              iff.elim_right le_iff_lt_or_eq (or.intro_left _ (lt_trans lt_ab lt_bc)))
+              iff.elim_right !strict_order_with_le.le_iff_lt_or_eq (or.intro_left _ (lt.trans lt_ab lt_bc)))
             (assume eq_bc : b = c, eq_bc ▸ le_ab))
         (assume eq_ab : a = b,
             eq_ab⁻¹ ▸ le_bc))
@@ -206,21 +213,25 @@ order_pair.mk
     assume le_ab : a ≤ b,
     assume le_ba : b ≤ a,
     show a = b, from
-      or.elim (le_imp_lt_or_eq le_ab)
+      or.elim (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ab)
         (assume lt_ab : a < b,
-          or.elim (le_imp_lt_or_eq le_ba)
-            (assume lt_ba : b < a, absurd (lt_trans lt_ab lt_ba) (lt_irrefl a))
+          or.elim (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ba)
+            (assume lt_ba : b < a, absurd (lt.trans lt_ab lt_ba) (lt.irrefl a))
             (assume eq_ba : b = a, eq_ba⁻¹))
         (assume eq_ab : a = b, eq_ab))
-  strong_order_pair.lt
+  strict_order_with_le.lt
   (take a b,
     iff.intro
       (assume lt_ab : a < b,
-        have le_ab : a ≤ b, from iff.elim_right le_iff_lt_or_eq (or.intro_left _ lt_ab),
-        show a ≤ b ∧ a ≠ b, from and.intro le_ab (lt_imp_ne lt_ab))
+        have le_ab : a ≤ b, from iff.elim_right !strict_order_with_le.le_iff_lt_or_eq (or.intro_left _ lt_ab),
+        show a ≤ b ∧ a ≠ b, from and.intro le_ab (lt.ne lt_ab))
       (assume H : a ≤ b ∧ a ≠ b,
-        have H1 : a < b ∨ a = b, from le_imp_lt_or_eq (and.elim_left H),
+        have H1 : a < b ∨ a = b, from iff.mp !strict_order_with_le.le_iff_lt_or_eq (and.elim_left H),
         show a < b, from or.resolve_left H1 (and.elim_right H)))
+  strict_order_with_le.le_iff_lt_or_eq
+
+
+/- linear orders -/
 
 structure linear_order_pair (A : Type) extends order_pair A, linear_weak_order A
 
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index b3aaa2639..3c592584c 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -36,27 +36,27 @@ section
   (add_comm c a) ▸ (add_comm c b) ▸ (add_le_left H c)
 
   theorem add_le {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d :=
-  le_trans (add_le_right Hab c) (add_le_left Hcd b)
+  le.trans (add_le_right Hab c) (add_le_left Hcd b)
 
   theorem add_lt_left {a b : A} (H : a < b) (c : A) : c + a < c + b :=
-  have H1 : c + a ≤ c + b, from add_le_left (lt_imp_le H) c,
+  have H1 : c + a ≤ c + b, from add_le_left (le_of_lt H) c,
   have H2 : c + a ≠ c + b, from
     take H3 : c + a = c + b,
     have H4 : a = b, from add_left_cancel H3,
-    lt_imp_ne H H4,
-  le_ne_imp_lt H1 H2
+    lt.ne H H4,
+  lt_of_le_of_ne H1 H2
 
   theorem add_lt_right {a b : A} (H : a < b) (c : A) : a + c < b + c :=
   (add_comm c a) ▸ (add_comm c b) ▸ (add_lt_left H c)
 
   theorem add_lt {a b c d : A} (Hab : a < b) (Hcd : c < d) : a + c < b + d :=
-  lt_trans (add_lt_right Hab c) (add_lt_left Hcd b)
+  lt.trans (add_lt_right Hab c) (add_lt_left Hcd b)
 
   theorem add_le_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d :=
-  le_lt_trans (add_le_right Hab c) (add_lt_left Hcd b)
+  lt_of_le_of_lt (add_le_right Hab c) (add_lt_left Hcd b)
 
   theorem add_lt_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d :=
-  lt_le_trans (add_lt_right Hab c) (add_le_left Hcd b)
+  lt_of_lt_of_le (add_lt_right Hab c) (add_le_left Hcd b)
 
   -- here we start using add_le_left_cancel.
   theorem add_le_left_cancel {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
@@ -66,10 +66,10 @@ section
   add_le_left_cancel ((add_comm a b) ▸ (add_comm c b) ▸ H)
 
   theorem add_lt_left_cancel {a b c : A} (H : a + b < a + c) : b < c :=
-  have H1 : b ≤ c, from add_le_left_cancel (lt_imp_le H),
+  have H1 : b ≤ c, from add_le_left_cancel (le_of_lt H),
   have H2 : b ≠ c, from
-    assume H3 : b = c, lt_irrefl _ (H3 ▸ H),
-  le_ne_imp_lt H1 H2
+    assume H3 : b = c, lt.irrefl _ (H3 ▸ H),
+  lt_of_le_of_ne H1 H2
 
   theorem add_lt_right_cancel {a b c : A} (H : a + b < c + b) : a < c :=
   add_lt_left_cancel ((add_comm a b) ▸ (add_comm c b) ▸ H)
@@ -101,7 +101,6 @@ section
 
   theorem add_nonpos_nonpos {a b : A} (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 :=
   !add_left_id ▸ (add_le Ha Hb)
-  calc_trans le_eq_trans
 
   theorem add_neg_nonpos {a b : A} (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 :=
   !add_left_id ▸ (add_lt_le Ha Hb)
@@ -121,13 +120,13 @@ section
           a = a + 0 : add_right_id
             ... ≤ a + b : add_le_left Hb
             ... = 0 : Hab,
-      have Haz : a = 0, from le_antisym Ha' Ha,
+      have Haz : a = 0, from le.antisym Ha' Ha,
       have Hb' : b ≤ 0, from
         calc
           b = 0 + b : add_left_id
             ... ≤ a + b : add_le_right Ha
             ... = 0 : Hab,
-      have Hbz : b = 0, from le_antisym Hb' Hb,
+      have Hbz : b = 0, from le.antisym Hb' Hb,
       and.intro Haz Hbz)
     (assume Hab : a = 0 ∧ b = 0,
       (and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add_right_id 0))
@@ -161,8 +160,8 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_
 definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] (A : Type)
     [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
 ordered_cancel_comm_monoid.mk has_add.add add_assoc !has_zero.zero add_left_id add_right_id add_comm
-(@add_left_cancel _ _) (@add_right_cancel _ _) has_le.le le_refl (@le_trans _ _) (@le_antisym _ _)
-has_lt.lt (@lt_iff_le_ne _ _) ordered_comm_group.add_le_left
+(@add_left_cancel _ _) (@add_right_cancel _ _) has_le.le le.refl (@le.trans _ _) (@le.antisym _ _)
+has_lt.lt (@lt_iff_le_and_ne _ _) ordered_comm_group.add_le_left
 proof
   take a b c : A,
   assume H : c + a ≤ c + b,