diff --git a/library/data/fin.lean b/library/data/fin.lean
index 82ec8ef911..667b449e87 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -61,7 +61,7 @@ namespace fin
                                 ...   = succ p₁                        : ih)
 
   private lemma of_nat_eq {p n : nat} (H : p < n) : n - succ p + succ p = n :=
-  add_sub_ge_left (lt_imp_le_succ H)
+  add_sub_ge_left (succ_le_of_lt H)
 
   definition of_nat (p : nat) (n : nat) : p < n → fin n :=
   λ H : p < n,
diff --git a/library/data/nat/decl.lean b/library/data/nat/decl.lean
index e0a73bc78c..6d1bdd2c15 100644
--- a/library/data/nat/decl.lean
+++ b/library/data/nat/decl.lean
@@ -18,9 +18,7 @@ namespace nat
 
   notation a < b := lt a b
 
-  inductive le (a : nat) : nat → Prop :=
-  refl    : le a a,
-  of_lt : ∀ {b}, lt a b → le a b
+  definition le (a b : nat) : Prop := a < succ b
 
   notation a ≤ b := le a b
 
@@ -94,25 +92,25 @@ namespace nat
       (λ b hl ih h₁ h₂, lt.step (ih h₁ h₂))),
   aux H₂ rfl H₁
 
-  definition lt.imp_succ {a b : nat} (H : a < b) : succ a < succ b :=
+  definition lt.succ_of_lt {a b : nat} (H : a < b) : succ a < succ b :=
   lt.rec_on H
     (lt.base (succ a))
     (λ b hlt ih, lt.trans ih (lt.base (succ b)))
 
-  definition lt.cancel_succ_left {a b : nat} (H : succ a < b) : a < b :=
+  definition lt.of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
   have aux : ∀ {a₁}, a₁ < b → succ a = a₁ → a < b, from
     λ a₁ H, lt.rec_on H
       (λ e₁, eq.rec_on e₁ (lt.step (lt.base a)))
       (λ d hlt ih e₁, lt.step (ih e₁)),
   aux H rfl
 
-  definition lt.cancel_succ_left_right {a b : nat} (H : succ a < succ b) : a < b :=
+  definition lt.of_succ_lt_succ {a b : nat} (H : succ a < succ b) : a < b :=
   have aux : pred (succ a) < pred (succ b), from
     lt.rec_on H
       (lt.base a)
       (λ (b : nat) (hlt : succ a < b) ih,
         show pred (succ a) < pred (succ b), from
-        lt.cancel_succ_left hlt),
+        lt.of_succ_lt hlt),
   aux
 
   definition lt.is_decidable_rel [instance] : decidable_rel lt :=
@@ -121,36 +119,55 @@ namespace nat
     (λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), cases_on a
        (inl !zero_lt_succ)
        (λ a, decidable.rec_on (ih a)
-         (λ h_pos : a < b₁, inl (lt.imp_succ h_pos))
+         (λ h_pos : a < b₁, inl (lt.succ_of_lt h_pos))
          (λ h_neg : ¬ a < b₁,
            have aux : ¬ succ a < succ b₁, from
-             λ h : succ a < succ b₁, h_neg (lt.cancel_succ_left_right h),
+             λ h : succ a < succ b₁, h_neg (lt.of_succ_lt_succ h),
            inr aux)))
     a
 
-  definition le_def_right {a b : nat} (H : a ≤ b) : a = b ∨ a < b :=
-  le.cases_on H
-    (or.inl rfl)
-    (λ b hlt, or.inr hlt)
+  definition le.refl (a : nat) : a ≤ a :=
+  lt.base a
 
-  definition le_def_left {a b : nat} (H : a = b ∨ a < b) : a ≤ b :=
+  definition le.of_lt {a b : nat} (H : a < b) : a ≤ b :=
+  lt.step H
+
+  definition eq_or_lt_of_le {a b : nat} (H : a ≤ b) : a = b ∨ a < b :=
+  begin
+    cases H with (b, hlt),
+      apply (or.inl rfl),
+      apply (or.inr hlt)
+  end
+
+  definition le.of_eq_or_lt {a b : nat} (H : a = b ∨ a < b) : a ≤ b :=
   or.rec_on H
     (λ hl, eq.rec_on hl !le.refl)
     (λ hr, le.of_lt hr)
 
   definition le.is_decidable_rel [instance] : decidable_rel le :=
-  λ a b, decidable_iff_equiv _ (iff.intro le_def_left le_def_right)
+  λ a b, decidable_iff_equiv _ (iff.intro le.of_eq_or_lt eq_or_lt_of_le)
+
+  inductive le2 (a : nat) : nat → Prop :=
+  refl    : le2 a a,
+  of_lt : ∀ {b}, lt a b → le2 a b
+
+  definition le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b :=
+  begin
+    cases H with (b', hlt),
+      apply H₁,
+      apply (H₂ b' hlt)
+  end
 
   definition lt.irrefl (a : nat) : ¬ a < a :=
   rec_on a
     !not_lt_zero
     (λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a),
-      ih (lt.cancel_succ_left_right h))
+      ih (lt.of_succ_lt_succ h))
 
   definition lt.asymm {a b : nat} (H : a < b) : ¬ b < a :=
   lt.rec_on H
-    (λ h : succ a < a, !lt.irrefl (lt.cancel_succ_left h))
-    (λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt.cancel_succ_left h))
+    (λ h : succ a < a, !lt.irrefl (lt.of_succ_lt h))
+    (λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt.of_succ_lt h))
 
   definition lt.trichotomy (a b : nat) : a < b ∨ a = b ∨ b < a :=
   rec_on b
@@ -160,74 +177,70 @@ namespace nat
     (λ b₁ (ih : ∀a, a < b₁ ∨ a = b₁ ∨ b₁ < a) (a : nat), cases_on a
        (or.inl !zero_lt_succ)
        (λ a, or.rec_on (ih a)
-           (λ h : a < b₁, or.inl (lt.imp_succ h))
+           (λ h : a < b₁, or.inl (lt.succ_of_lt h))
            (λ h, or.rec_on h
               (λ h : a = b₁, or.inr (or.inl (eq.rec_on h rfl)))
-              (λ h : b₁ < a, or.inr (or.inr (lt.imp_succ h))))))
+              (λ h : b₁ < a, or.inr (or.inr (lt.succ_of_lt h))))))
     a
 
-  definition not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ∨ b < a :=
+  definition eq_or_lt_of_not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ∨ b < a :=
   or.rec_on (lt.trichotomy a b)
     (λ hlt, absurd hlt hnlt)
     (λ h, h)
 
-  definition le_imp_lt_succ {a b : nat} (h : a ≤ b) : a < succ b :=
-  le.rec_on h
-    (lt.base a)
-    (λ b h, lt.step h)
+  definition lt_succ_of_le {a b : nat} (h : a ≤ b) : a < succ b :=
+  h
 
-  definition le_succ_imp_lt {a b : nat} (h : succ a ≤ b) : a < b :=
-  le.rec_on h
-    (lt.base a)
-    (λ b (h : succ a < b), lt.cancel_succ_left_right (lt.step h))
+  definition lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
+  lt.of_succ_lt_succ h
 
   definition le.step {a b : nat} (h : a ≤ b) : a ≤ succ b :=
-  le.rec_on h
-    (le.of_lt (lt.base a))
-    (λ b (h : a < b), le.of_lt (lt.step h))
+  lt.step h
 
-  definition lt_imp_le_succ {a b : nat} (h : a < b) : succ a ≤ b :=
-  lt.rec_on h
-    (le.refl (succ a))
-    (λ b hlt (ih : succ a ≤ b), le.step ih)
+  definition succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
+  lt.succ_of_lt h
 
-  definition le.trans {a b c : nat} (h₁ : a ≤ b) : b ≤ c → a ≤ c :=
-  le.rec_on h₁
-    (λ h, h)
-    (λ b (h₁ : a < b) (h₂ : b ≤ c), le.rec_on h₂
-      (le.of_lt h₁)
-      (λ c (h₂ : b < c), le.of_lt (lt.trans h₁ h₂)))
+  definition le.trans {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
+  begin
+    cases h₁ with (b', hlt),
+      apply h₂,
+      apply (lt.trans hlt h₂)
+  end
 
-  definition le_lt.trans {a b c : nat} (h₁ : a ≤ b) : b < c → a < c :=
-  le.rec_on h₁
-    (λ h, h)
-    (λ b (h₁ : a < b) (h₂ : b < c), lt.trans h₁ h₂)
+  definition lt.of_le_of_lt {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
+  begin
+    cases h₁ with (b', hlt),
+      apply h₂,
+      apply (lt.trans hlt h₂)
+  end
 
-  definition lt_le.trans {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
-  le.rec_on h₂
-    h₁
-    (λ c (h₂ : b < c), lt.trans h₁ h₂)
+  definition lt.of_lt_of_le {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
+  begin
+    cases h₁ with (b', hlt),
+      apply (lt.of_succ_lt_succ h₂),
+      apply (lt.trans hlt (lt.of_succ_lt_succ h₂))
+  end
 
-  definition lt_eq.trans {a b c : nat} (h₁ : a < b) (h₂ : b = c) : a < c :=
+  definition lt.of_lt_of_eq {a b c : nat} (h₁ : a < b) (h₂ : b = c) : a < c :=
   eq.rec_on h₂ h₁
 
-  definition le_eq.trans {a b c : nat} (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c :=
+  definition le.of_le_of_eq {a b c : nat} (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c :=
   eq.rec_on h₂ h₁
 
-  definition eq_lt.trans {a b c : nat} (h₁ : a = b) (h₂ : b < c) : a < c :=
+  definition lt.of_eq_of_lt {a b c : nat} (h₁ : a = b) (h₂ : b < c) : a < c :=
   eq.rec_on (eq.rec_on h₁ rfl) h₂
 
-  definition eq_le.trans {a b c : nat} (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c :=
+  definition le.of_eq_of_le {a b c : nat} (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c :=
   eq.rec_on (eq.rec_on h₁ rfl) h₂
 
   calc_trans lt.trans
+  calc_trans lt.of_le_of_lt
+  calc_trans lt.of_lt_of_le
+  calc_trans lt.of_lt_of_eq
+  calc_trans lt.of_eq_of_lt
   calc_trans le.trans
-  calc_trans le_lt.trans
-  calc_trans lt_le.trans
-  calc_trans lt_eq.trans
-  calc_trans le_eq.trans
-  calc_trans eq_lt.trans
-  calc_trans eq_le.trans
+  calc_trans le.of_le_of_eq
+  calc_trans le.of_eq_of_le
 
   definition max (a b : nat) : nat :=
   if a < b then b else a
@@ -244,24 +257,24 @@ namespace nat
   definition max.eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
   if_neg H
 
-  definition max.eq_right_symm {a b : nat} (H : a < b) : b = max a b :=
+  definition max.right_eq {a b : nat} (H : a < b) : b = max a b :=
   eq.rec_on (max.eq_right H) rfl
 
-  definition max.eq_left_symm {a b : nat} (H : ¬ a < b) : a = max a b :=
+  definition max.left_eq {a b : nat} (H : ¬ a < b) : a = max a b :=
   eq.rec_on (max.eq_left H) rfl
 
   definition max.left (a b : nat) : a ≤ max a b :=
   by_cases
-    (λ h : a < b,   le.of_lt (eq.rec_on (max.eq_right_symm h) h))
+    (λ h : a < b,   le.of_lt (eq.rec_on (max.right_eq h) h))
     (λ h : ¬ a < b, eq.rec_on (max.eq_left h) !le.refl)
 
   definition max.right (a b : nat) : b ≤ max a b :=
   by_cases
     (λ h : a < b,   eq.rec_on (max.eq_right h) !le.refl)
-    (λ h : ¬ a < b, or.rec_on (not_lt h)
+    (λ h : ¬ a < b, or.rec_on (eq_or_lt_of_not_lt h)
       (λ heq, eq.rec_on heq (eq.rec_on (max_a_a a) !le.refl))
       (λ h : b < a,
-        have aux : a = max a b, from max.eq_left_symm (lt.asymm h),
+        have aux : a = max a b, from max.left_eq (lt.asymm h),
         eq.rec_on aux (le.of_lt h)))
 
   definition gt a b := lt b a
@@ -287,23 +300,23 @@ namespace nat
 
   notation a * b := mul a b
 
-  definition sub.succ_succ (a b : nat) : succ a - succ b = a - b :=
+  definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
   induction_on b
     rfl
     (λ b₁ (ih : succ a - succ b₁ = a - b₁),
       eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
 
-  definition sub.succ_succ_symm (a b : nat) : a - b = succ a - succ b :=
-  eq.rec_on (sub.succ_succ a b) rfl
+  definition sub_eq_succ_sub_succ (a b : nat) : a - b = succ a - succ b :=
+  eq.rec_on (succ_sub_succ_eq_sub a b) rfl
 
-  definition sub.zero_left (a : nat) : zero - a = zero :=
+  definition zero_sub_eq_zero (a : nat) : zero - a = zero :=
   induction_on a
     rfl
     (λ a₁ (ih : zero - a₁ = zero),
       eq.rec_on ih (eq.refl (pred (zero - a₁))))
 
-  definition sub.zero_left_symm (a : nat) : zero = zero - a :=
-  eq.rec_on (sub.zero_left a) rfl
+  definition zero_eq_zero_sub (a : nat) : zero = zero - a :=
+  eq.rec_on (zero_sub_eq_zero a) rfl
 
   definition sub.lt {a b : nat} : zero < a → zero < b → a - b < a :=
   have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
@@ -311,23 +324,23 @@ namespace nat
       (λb h₂, lt.cases_on h₂
         (lt.base zero)
         (λ b₁ bpos,
-          eq.rec_on (sub.succ_succ_symm zero b₁)
-           (eq.rec_on (sub.zero_left_symm b₁) (lt.base zero))))
+          eq.rec_on (sub_eq_succ_sub_succ zero b₁)
+           (eq.rec_on (zero_eq_zero_sub b₁) (lt.base zero))))
       (λa₁ apos ih b h₂, lt.cases_on h₂
         (lt.base a₁)
         (λ b₁ bpos,
-          eq.rec_on (sub.succ_succ_symm a₁ b₁)
+          eq.rec_on (sub_eq_succ_sub_succ a₁ b₁)
             (lt.trans (@ih b₁ bpos) (lt.base a₁)))),
   λ h₁ h₂, aux h₁ h₂
 
-  definition sub_pred (a : nat) : pred a ≤ a :=
+  definition pred_le (a : nat) : pred a ≤ a :=
   cases_on a
     (le.refl zero)
     (λ a₁, le.of_lt (lt.base a₁))
 
-  definition sub_le_self (a b : nat) : a - b ≤ a :=
+  definition sub_le (a b : nat) : a - b ≤ a :=
   induction_on b
     (le.refl a)
-    (λ b₁ ih, le.trans !sub_pred ih)
+    (λ b₁ ih, le.trans !pred_le ih)
 
 end nat
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index ed5f911dbf..ac7b3370fb 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -20,7 +20,7 @@ namespace nat
 -- Auxiliary lemma used to justify div
 private definition div_rec_lemma {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
 and.rec_on H (λ ypos ylex,
-  sub.lt (lt_le.trans ypos ylex) ypos)
+  sub.lt (lt.of_lt_of_le ypos ylex) ypos)
 
 private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
 dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y) (div_rec_lemma Hp) y + 1) else (λ Hn, zero)
@@ -40,7 +40,7 @@ theorem div_less {a b : ℕ} (h : a < b) : a div b = 0 :=
 divide_def a b ⬝ if_neg (!and.not_right (lt_imp_not_ge h))
 
 theorem zero_div (b : ℕ) : 0 div b = 0 :=
-divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_le.trans l r) (lt.irrefl 0)))
+divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt.of_lt_of_le l r) (lt.irrefl 0)))
 
 theorem div_rec {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a div b = succ ((a - b) div b) :=
 divide_def a b ⬝ if_pos (and.intro h₁ h₂)
@@ -80,7 +80,7 @@ theorem mod_less {a b : ℕ} (h : a < b) : a mod b = a :=
 modulo_def a b ⬝ if_neg (!and.not_right (lt_imp_not_ge h))
 
 theorem zero_mod (b : ℕ) : 0 mod b = 0 :=
-modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_le.trans l r) (lt.irrefl 0)))
+modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt.of_lt_of_le l r) (lt.irrefl 0)))
 
 theorem mod_rec {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a mod b = (a - b) mod b :=
 modulo_def a b ⬝ if_pos (and.intro h₁ h₂)
@@ -187,7 +187,7 @@ theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y)
   (H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 :=
 have H4 : q1 * y + r2 = q2 * y + r2, from (remainder_unique H H1 H2 H3) ▸ H3,
 have H5 : q1 * y = q2 * y, from add.cancel_right H4,
-have H6 : y > 0, from le_lt.trans !zero_le H1,
+have H6 : y > 0, from lt.of_le_of_lt !zero_le H1,
 show q1 = q2, from mul_cancel_right H6 H5
 
 theorem div_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y :=
@@ -256,7 +256,7 @@ definition dvd (x y : ℕ) : Prop := y mod x = 0
 infix `|` := dvd
 
 theorem dvd_iff_mod_eq_zero {x y : ℕ} : x | y ↔ y mod x = 0 :=
-eq_to_iff rfl
+iff.of_eq rfl
 
 theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x :=
 (calc
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 839e0844d5..2ac912b135 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -17,9 +17,7 @@ namespace nat
 -- ------------------
 
 theorem le.succ_right {n m : ℕ} (h : n ≤ m) : n ≤ succ m :=
-le.rec_on h
-  (le.of_lt (lt.base n))
-  (λ b (h : n < b), le.of_lt (lt.step h))
+lt.step h
 
 theorem le.add_right (n k : ℕ) : n ≤ n + k :=
 induction_on k
@@ -179,7 +177,7 @@ case n
   (pred.zero⁻¹ ▸ !le_refl)
   (take k : ℕ, !pred.succ⁻¹ ▸ !self_le_succ)
 
-theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
+theorem pred_le_pre_of_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
 discriminate
   (take Hn : n = 0,
     have H2 : pred n = 0,
@@ -237,10 +235,10 @@ le_trans (mul_le_right H1 m) (mul_le_left H2 k)
 -- ----------------------------------------------
 
 theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
-le_succ_imp_lt (le_intro H)
+lt_of_succ_le (le_intro H)
 
 theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m :=
-le_elim (lt_imp_le_succ H)
+le_elim (succ_le_of_lt H)
 
 theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
 lt_intro !add.move_succ
@@ -255,8 +253,8 @@ not_intro (assume H : n < n, absurd rfl (lt_imp_ne H))
 
 theorem lt_def (n m : ℕ) : n < m ↔ succ n ≤ m :=
 iff.intro
-  (λ h, lt_imp_le_succ h)
-  (λ h, le_succ_imp_lt h)
+  (λ h, succ_le_of_lt h)
+  (λ h, lt_of_succ_le h)
 
 theorem succ_pos (n : ℕ) : 0 < succ n :=
 !zero_lt_succ
@@ -275,13 +273,13 @@ theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m :=
 le.of_lt H
 
 theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m :=
-or.swap (le_def_right H)
+or.swap (eq_or_lt_of_le H)
 
 theorem le_ne_imp_lt {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : n < m :=
 or.resolve_left (le_imp_lt_or_eq H1) H2
 
 theorem lt_succ_imp_le {n m : ℕ} (H : n < succ m) : n ≤ m :=
-succ_le_cancel (lt_imp_le_succ H)
+succ_le_cancel (succ_le_of_lt H)
 
 theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m :=
 le.rec_on H
@@ -289,7 +287,7 @@ le.rec_on H
   (λ m (h : n < m), lt.asymm h)
 
 theorem lt_imp_not_ge {n m : ℕ} (H : n < m) : ¬ n ≥ m :=
-not_intro (assume H2 : m ≤ n, absurd (lt_le.trans H H2) !lt_irrefl)
+not_intro (assume H2 : m ≤ n, absurd (lt.of_lt_of_le H H2) !lt_irrefl)
 
 theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n :=
 lt.asymm H
@@ -299,22 +297,22 @@ lt.asymm H
 -- ### interaction with addition
 
 theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
-le_succ_imp_lt (!add.succ_right ▸ add_le_left (lt_imp_le_succ H) k)
+lt_of_succ_le (!add.succ_right ▸ add_le_left (succ_le_of_lt H) k)
 
 theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
 !add.comm ▸ !add.comm ▸ add_lt_left H k
 
 theorem add_le_lt {n m k l : ℕ} (H1 : n ≤ k) (H2 : m < l) : n + m < k + l :=
-le_lt.trans (add_le_right H1 m) (add_lt_left H2 k)
+lt.of_le_of_lt (add_le_right H1 m) (add_lt_left H2 k)
 
 theorem add_lt_le {n m k l : ℕ} (H1 : n < k) (H2 : m ≤ l) : n + m < k + l :=
-lt_le.trans (add_lt_right H1 m) (add_le_left H2 k)
+lt.of_lt_of_le (add_lt_right H1 m) (add_le_left H2 k)
 
 theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l :=
 add_lt_le H1 (lt_imp_le H2)
 
 theorem add_lt_cancel_left {n m k : ℕ} (H : k + n < k + m) : n < m :=
-le_succ_imp_lt (add_le_cancel_left (!add.succ_right⁻¹ ▸ (lt_imp_le_succ H)))
+lt_of_succ_le (add_le_cancel_left (!add.succ_right⁻¹ ▸ (succ_le_of_lt H)))
 
 theorem add_lt_cancel_right {n m k : ℕ} (H : n + k < m + k) : n < m :=
 add_lt_cancel_left (!add.comm ▸ !add.comm ▸ H)
@@ -386,7 +384,7 @@ strong_induction_on a (
        (take n,
          assume H : (∀m, m < succ n → P m),
          show P (succ n), from
-           Hind n (take m, assume H1 : m ≤ n, H _ (le_imp_lt_succ H1))))
+           Hind n (take m, assume H1 : m ≤ n, H _ (lt_succ_of_le H1))))
 
 -- Positivity
 -- ---------
@@ -452,22 +450,22 @@ mul_pos_imp_pos_left (!mul.comm ▸ H)
 
 theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m :=
 have H2 : k * n < k * n + k, from add_pos_right Hk,
-have H3 : k * n + k ≤ k * m, from !mul.succ_right ▸ mul_le_left (lt_imp_le_succ H) k,
-lt_le.trans H2 H3
+have H3 : k * n + k ≤ k * m, from !mul.succ_right ▸ mul_le_left (succ_le_of_lt H) k,
+lt.of_lt_of_le H2 H3
 
 theorem mul_lt_right {n m k : ℕ} (Hk : k > 0) (H : n < m)  : n * k < m * k :=
 !mul.comm ▸ !mul.comm ▸ mul_lt_left Hk H
 
 theorem mul_le_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) : n * m < k * l :=
-le_lt.trans (mul_le_right H1 m) (mul_lt_left Hk H2)
+lt.of_le_of_lt (mul_le_right H1 m) (mul_lt_left Hk H2)
 
 theorem mul_lt_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l :=
-le_lt.trans (mul_le_left H2 n) (mul_lt_right Hl H1)
+lt.of_le_of_lt (mul_le_left H2 n) (mul_lt_right Hl H1)
 
 theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
 have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m,
-have H4 : k * m < k * l, from mul_lt_left (le_lt.trans !zero_le H1) H2,
-le_lt.trans H3 H4
+have H4 : k * m < k * l, from mul_lt_left (lt.of_le_of_lt !zero_le H1) H2,
+lt.of_le_of_lt H3 H4
 
 theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
 or.elim le_or_gt
@@ -480,7 +478,7 @@ theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m :=
 mul_lt_cancel_left (!mul.comm ▸ !mul.comm ▸ H)
 
 theorem mul_le_cancel_left {n m k : ℕ} (Hk : k > 0) (H : k * n ≤ k * m) : n ≤ m :=
-have H2 : k * n < k * m + k, from le_lt.trans H (add_pos_right Hk),
+have H2 : k * n < k * m + k, from lt.of_le_of_lt H (add_pos_right Hk),
 have H3 : k * n < k * succ m, from !mul.succ_right⁻¹ ▸ H2,
 have H4 : n < succ m, from mul_lt_cancel_left H3,
 show n ≤ m, from lt_succ_imp_le H4
@@ -511,9 +509,9 @@ have H3 : n > 0, from mul_pos_imp_pos_left H2,
 have H4 : m > 0, from mul_pos_imp_pos_right H2,
 or.elim le_or_gt
   (assume H5 : n ≤ 1,
-    show n = 1, from le_antisym H5 (lt_imp_le_succ H3))
+    show n = 1, from le_antisym H5 (succ_le_of_lt H3))
   (assume H5 : n > 1,
-    have H6 : n * m ≥ 2 * 1, from mul_le (lt_imp_le_succ H5) (lt_imp_le_succ H4),
+    have H6 : n * m ≥ 2 * 1, from mul_le (succ_le_of_lt H5) (succ_le_of_lt H4),
     have H7 : 1 ≥ 2, from !mul.one_right ▸ H ▸ H6,
     absurd !self_lt_succ (le_imp_not_gt H7))
 
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 1624b43c52..eeeee7dd25 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -36,7 +36,7 @@ induction_on n !sub_zero_right
              ... = 0            : pred.zero)
 
 theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m :=
-sub.succ_succ n m
+succ_sub_succ_eq_sub n m
 
 theorem sub_self (n : ℕ) : n - n = 0 :=
 induction_on n !sub_zero_right (take k IH, !sub_succ_succ ⬝ IH)
diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean
index ad0fefa80c..7729f8229d 100644
--- a/library/data/quotient/classical.lean
+++ b/library/data/quotient/classical.lean
@@ -35,7 +35,7 @@ have H3 : ∀c, R a c ↔ R b c, from
       (assume H4 : R a c, transR (symmR H2) H4)
       (assume H4 : R b c, transR H2 H4),
 have H4 : (fun c, R a c) = (fun c, R b c), from
-  funext (take c, iff_to_eq (H3 c)),
+  funext (take c, eq.of_iff (H3 c)),
 have H5 [visible] : nonempty A, from
   nonempty.intro a,
 show epsilon (λc, R a c) = epsilon (λc, R b c), from
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index b05db0d9da..19c6caba10 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -41,17 +41,17 @@ or.elim (prop_complete a)
     (assume Hbt,  false_elim (Haf ▸ (Hba (eq_true_elim Hbt))))
     (assume Hbf, Haf ⬝ Hbf⁻¹))
 
-theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b :=
+theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
 iff.elim (assume H1 H2, propext H1 H2) H
 
 theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
 propext
-  (assume H, iff_to_eq H)
-  (assume H, eq_to_iff H)
+  (assume H, eq.of_iff H)
+  (assume H, iff.of_eq H)
 
 open relation
 theorem iff_congruence [instance] (P : Prop → Prop) : is_congruence iff iff P :=
 is_congruence.mk
   (take (a b : Prop),
     assume H : a ↔ b,
-    show P a ↔ P b, from eq_to_iff (iff_to_eq H ▸ eq.refl (P a)))
+    show P a ↔ P b, from iff.of_eq (eq.of_iff H ▸ eq.refl (P a)))
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
index b604a9496e..d380f20260 100644
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@@ -152,16 +152,15 @@ namespace iff
 
   theorem false_elim (H : a ↔ false) : ¬a :=
   assume Ha : a, mp H Ha
+
+  open eq.ops
+  theorem of_eq {a b : Prop} (H : a = b) : a ↔ b :=
+  iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
 end iff
 
 calc_refl iff.refl
 calc_trans iff.trans
 
-open eq.ops
-
-theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
-iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
-
 -- comm and assoc for and / or
 -- ---------------------------
 namespace and
diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean
index 3c19f0bcad..31ce10560d 100644
--- a/library/logic/decidable.lean
+++ b/library/logic/decidable.lean
@@ -83,7 +83,7 @@ namespace decidable
     (assume Hnp : ¬p, inr (iff.elim_left (iff.flip_sign H) Hnp))
 
   definition decidable_eq_equiv (Hp : decidable p) (H : p = q) : decidable q :=
-  decidable_iff_equiv Hp (eq_to_iff H)
+  decidable_iff_equiv Hp (iff.of_eq H)
 
   protected theorem rec_subsingleton [instance] [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type}
       (H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index 82bb730f75..144cd38189 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -78,7 +78,7 @@ case_strong_induction_on m
               assume Hzx : measure z < measure x,
               calc
                 f' m z = restrict default measure f m z : IH m !le_refl z
-                  ... = f z : !restrict_lt_eq (lt_le.trans Hzx (lt_succ_imp_le H1))
+                  ... = f z : !restrict_lt_eq (lt.of_lt_of_le Hzx (lt_succ_imp_le H1))
           ∎,
           have H2 : f' (succ m) x = rec_val x f,
           proof
diff --git a/tests/lean/run/div_wf.lean b/tests/lean/run/div_wf.lean
index 04790adaa1..5ef03ae68c 100644
--- a/tests/lean/run/div_wf.lean
+++ b/tests/lean/run/div_wf.lean
@@ -4,7 +4,7 @@ open nat well_founded decidable prod eq.ops
 -- Auxiliary lemma used to justify recursive call
 private definition lt_aux {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
 and.rec_on H (λ ypos ylex,
-  sub.lt (lt_le.trans ypos ylex) ypos)
+  sub.lt (lt.of_lt_of_le ypos ylex) ypos)
 
 definition wdiv.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
 dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y) (lt_aux Hp) y + 1) else (λ Hn, zero)
diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean
index cf95938281..3a01e9e493 100644
--- a/tests/lean/run/forest_height.lean
+++ b/tests/lean/run/forest_height.lean
@@ -42,12 +42,12 @@ aux
 
 definition tree_forest.height_lt.cons₁ {A : Type} (t : tree A) (f : forest A) : sum.inl _ t ≺ sum.inr _ (forest.cons t f) :=
 have aux : tree.height t < forest.height (forest.cons t f), from
-  le_imp_lt_succ (max.left _ _),
+  lt_succ_of_le (max.left _ _),
 aux
 
 definition tree_forest.height_lt.cons₂ {A : Type} (t : tree A) (f : forest A) : sum.inr _ f ≺ sum.inr _ (forest.cons t f) :=
 have aux : forest.height f < forest.height (forest.cons t f), from
-  le_imp_lt_succ (max.right _ _),
+  lt_succ_of_le (max.right _ _),
 aux
 
 definition kind {A : Type} (t : tree_forest A) : bool :=
diff --git a/tests/lean/run/gcd.lean b/tests/lean/run/gcd.lean
index ade5f30cd9..f81fc8eeb7 100644
--- a/tests/lean/run/gcd.lean
+++ b/tests/lean/run/gcd.lean
@@ -11,11 +11,11 @@ infixl `≺`:50 := pair_nat.lt
 
 -- Lemma for justifying recursive call
 private lemma lt₁ (x₁ y₁ : nat) : (x₁ - y₁, succ y₁) ≺ (succ x₁, succ y₁) :=
-!lex.left (le_imp_lt_succ (sub_le_self x₁ y₁))
+!lex.left (lt_succ_of_le (sub_le x₁ y₁))
 
 -- Lemma for justifying recursive call
 private lemma lt₂ (x₁ y₁ : nat) : (succ x₁, y₁ - x₁) ≺ (succ x₁, succ y₁) :=
-!lex.right (le_imp_lt_succ (sub_le_self y₁ x₁))
+!lex.right (lt_succ_of_le (sub_le y₁ x₁))
 
 definition gcd.F (p₁ : nat × nat) : (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat :=
 prod.cases_on p₁ (λ (x y : nat),
diff --git a/tests/lean/run/tree_height.lean b/tests/lean/run/tree_height.lean
index 02f4b43fde..1393abf0f3 100644
--- a/tests/lean/run/tree_height.lean
+++ b/tests/lean/run/tree_height.lean
@@ -19,10 +19,10 @@ definition height_lt.wf (A : Type) : well_founded (@height_lt A) :=
 inv_image.wf height lt.wf
 
 theorem height_lt.node_left {A : Type} (t₁ t₂ : tree A) : height_lt t₁ (node t₁ t₂) :=
-le_imp_lt_succ (max.left (height t₁) (height t₂))
+lt_succ_of_le (max.left (height t₁) (height t₂))
 
 theorem height_lt.node_right {A : Type} (t₁ t₂ : tree A) : height_lt t₂ (node t₁ t₂) :=
-le_imp_lt_succ (max.right (height t₁) (height t₂))
+lt_succ_of_le (max.right (height t₁) (height t₂))
 
 theorem height_lt.trans {A : Type} : transitive (@height_lt A) :=
 inv_image.trans lt height @lt.trans