From 064ecd3e3d1429e8f4baa2f74450dccf7eff7fd9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 Nov 2014 00:15:51 -0800
Subject: [PATCH] refactor(library/data/nat): declare lt and le asap using
 inductive definitions, and make key theorems transparent for definitional
 package

We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.
---
 library/data/fin.lean             |   4 +-
 library/data/int/order.lean       |   2 +-
 library/data/nat/basic.lean       |  94 +++-------
 library/data/nat/decl.lean        | 277 ++++++++++++++++++++++++++++++
 library/data/nat/default.lean     |   2 +-
 library/data/nat/div.lean         |  10 +-
 library/data/nat/order.lean       | 243 ++++++++------------------
 library/data/nat/sub.lean         |  64 +++----
 library/data/nat/wf.lean          |  52 ------
 tests/lean/notation.lean          |   2 +-
 tests/lean/run/div2.lean          |   2 +-
 tests/lean/run/div_wf.lean        |   2 +-
 tests/lean/run/fib_wrec.lean      |  12 +-
 tests/lean/run/tree_height.lean   |   6 +-
 tests/lean/whnf.lean.expected.out |   4 +-
 15 files changed, 426 insertions(+), 350 deletions(-)
 create mode 100644 library/data/nat/decl.lean
 delete mode 100644 library/data/nat/wf.lean

diff --git a/library/data/fin.lean b/library/data/fin.lean
index 6ec15740f..e34e918b8 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -74,8 +74,8 @@ namespace fin
        to_nat (of_nat_core (succ p₁)) = succ (to_nat (of_nat_core p₁)) : rfl
                                 ...   = succ p₁                        : ih)
 
-  private lemma of_nat_eq {p : nat} {n : nat} (H : p < n) : n - succ p + succ p = n :=
-  add_sub_ge_left (eq.subst (lt_def p n) H)
+  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)
 
   definition of_nat (p : nat) (n : nat) : p < n → fin n :=
   λ H : p < n,
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index c67de322a..37279d254 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -235,7 +235,7 @@ theorem lt_of_nat (n m : ℕ) : (of_nat n < of_nat m) ↔ (n < m) :=
 calc
   (of_nat n + 1 ≤ of_nat m) ↔ (of_nat (succ n) ≤ of_nat m) : by simp
     ... ↔ (succ n ≤ m) : le_of_nat (succ n) m
-    ... ↔ (n < m) : iff.symm (eq_to_iff (nat.lt_def n m))
+    ... ↔ (n < m) : iff.symm (nat.lt_def n m)
 
 theorem gt_of_nat (n m : ℕ) : (of_nat n > of_nat m) ↔ (n > m) :=
 lt_of_nat m n
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 13abdb61c..d0f071083 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -1,44 +1,18 @@
 --- Copyright (c) 2014 Floris van Doorn. All rights reserved.
 --- Released under Apache 2.0 license as described in the file LICENSE.
---- Author: Floris van Doorn
+--- Author: Floris van Doorn, Leonardo de Moura
 
--- data.nat.basic
--- ==============
---
 -- Basic operations on the natural numbers.
 
-import logic data.num tools.tactic algebra.binary tools.helper_tactics
-import logic.inhabited
+import .decl data.num algebra.binary
 
-open tactic binary eq.ops
-open decidable
-open relation -- for subst_iff
-open helper_tactics
-
--- Definition of the type
--- ----------------------
-inductive nat : Type :=
-  zero : nat,
-  succ : nat → nat
+open eq.ops binary
 
 namespace nat
 
-notation `ℕ` := nat
-
-theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat.rec x f zero = x
-
-theorem rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) :
-  nat.rec x f (succ n) = f n (nat.rec x f n)
-
-protected definition is_inhabited [instance] : inhabited nat :=
-inhabited.mk zero
-
--- Coercion from num
--- -----------------
-
-definition add (x y : ℕ) : ℕ :=
-nat.rec x (λ n r, succ r) y
-notation a + b := add a b
+definition of_num [coercion] [reducible] (n : num) : ℕ :=
+num.rec zero
+  (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
 
 definition addl (x y : ℕ) : ℕ :=
 nat.rec y (λ n r, succ r) x
@@ -70,10 +44,6 @@ nat.induction_on x
                    ...  = succ (succ x₁ ⊕ y₁) : {ih₂}
                    ...  = succ x₁ ⊕ succ y₁   : addl.succ_right))
 
-definition of_num [coercion] [reducible] (n : num) : ℕ :=
-num.rec zero
-    (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
-
 -- Successor and predecessor
 -- -------------------------
 
@@ -82,11 +52,11 @@ assume H, no_confusion H
 
 -- add_rewrite succ_ne_zero
 
-definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n
+theorem pred.zero : pred 0 = 0 :=
+rfl
 
-theorem pred.zero : pred 0 = 0
-
-theorem pred.succ (n : ℕ) : pred (succ n) = n
+theorem pred.succ (n : ℕ) : pred (succ n) = n :=
+rfl
 
 irreducible pred
 
@@ -103,11 +73,6 @@ or.imp_or (zero_or_succ_pred n) (assume H, H)
 theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n :=
 induction_on n H1 (take m IH, H2 m)
 
-theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
-or.elim (zero_or_succ_pred n)
-  (take H3 : n = 0, H1 H3)
-  (take H3 : n = succ (pred n), H2 (pred n) H3)
-
 theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
 no_confusion H (λe, e)
 
@@ -118,25 +83,11 @@ induction_on n
     absurd H ne)
   (take k IH H, IH (succ.inj H))
 
-protected definition has_decidable_eq [instance] : decidable_eq ℕ :=
-take n m : ℕ,
-have general : ∀n, decidable (n = m), from
-  rec_on m
-    (take n,
-      rec_on n
-        (inl rfl)
-        (λ m iH, inr !succ_ne_zero))
-    (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')),
-      take n, rec_on n
-        (inr (ne.symm !succ_ne_zero))
-        (λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
-          decidable.by_cases
-            (assume Heq : n' = m', inl (congr_arg succ Heq))
-            (assume Hne : n' ≠ m',
-              have H1 : succ n' ≠ succ m', from
-                assume Heq, absurd (succ.inj Heq) Hne,
-              inr H1))),
-general n
+
+theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
+or.elim (zero_or_succ_pred n)
+  (take H3 : n = 0, H1 H3)
+  (take H3 : n = succ (pred n), H2 (pred n) H3)
 
 theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1)
     (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a :=
@@ -163,9 +114,11 @@ general m
 
 -- Addition
 -- --------
-theorem add.zero_right (n : ℕ) : n + 0 = n
+theorem add.zero_right (n : ℕ) : n + 0 = n :=
+rfl
 
-theorem add.succ_right (n m : ℕ) : n + succ m = succ (n + m)
+theorem add.succ_right (n m : ℕ) : n + succ m = succ (n + m) :=
+rfl
 
 irreducible add
 
@@ -267,12 +220,11 @@ nat.rec H1 (take n IH, !add.one ▸ (H2 n IH)) a
 -- Multiplication
 -- --------------
 
-definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
-notation a * b := mul a b
+theorem mul.zero_right (n : ℕ) : n * 0 = 0 :=
+rfl
 
-theorem mul.zero_right (n : ℕ) : n * 0 = 0
-
-theorem mul.succ_right (n m : ℕ) : n * succ m = n * m + n
+theorem mul.succ_right (n m : ℕ) : n * succ m = n * m + n :=
+rfl
 
 irreducible mul
 
diff --git a/library/data/nat/decl.lean b/library/data/nat/decl.lean
new file mode 100644
index 000000000..f022b25ff
--- /dev/null
+++ b/library/data/nat/decl.lean
@@ -0,0 +1,277 @@
+--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Floris van Doorn, Leonardo de Moura
+import logic.eq logic.heq logic.wf logic.decidable logic.if data.prod
+
+open eq.ops decidable
+
+inductive nat :=
+zero : nat,
+succ : nat → nat
+
+namespace nat
+  notation `ℕ` := nat
+
+  inductive lt (a : nat) : nat → Prop :=
+  base : lt a (succ a),
+  step : Π {b}, lt a b → lt a (succ b)
+
+  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
+
+  notation a ≤ b := le a b
+
+  definition pred (a : nat) : nat :=
+  cases_on a zero (λ a₁, a₁)
+
+  protected definition is_inhabited [instance] : inhabited nat :=
+  inhabited.mk zero
+
+  protected definition has_decidable_eq [instance] : decidable_eq nat :=
+  λn m : nat,
+  have general : ∀n, decidable (n = m), from
+    rec_on m
+      (λ n, cases_on n
+        (inl rfl)
+        (λ m, inr (λ (e : succ m = zero), no_confusion e)))
+      (λ (m' : nat) (ih : ∀n, decidable (n = m')) (n : nat), cases_on n
+        (inr (λ h, no_confusion h))
+        (λ (n' : nat),
+          decidable.rec_on (ih n')
+            (assume Heq : n' = m', inl (eq.rec_on Heq rfl))
+            (assume Hne : n' ≠ m',
+              have H1 : succ n' ≠ succ m', from
+                assume Heq, no_confusion Heq (λ e : n' = m', Hne e),
+              inr H1))),
+  general n
+
+  -- less-than is well-founded
+  definition lt.wf [instance] : well_founded lt :=
+  well_founded.intro (λn, rec_on n
+    (acc.intro zero (λ (y : nat) (hlt : y < zero),
+      have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from
+        λ n₁ hlt, lt.cases_on hlt
+          (λ heq, no_confusion heq)
+          (λ b hlt heq, no_confusion heq),
+      aux hlt rfl))
+    (λ (n : nat) (ih : acc lt n),
+      acc.intro (succ n) (λ (m : nat) (hlt : m < succ n),
+        have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from
+          λ n₁ hlt, lt.cases_on hlt
+            (λ (heq : succ n = succ m),
+              nat.no_confusion heq (λ (e : n = m),
+                eq.rec_on e ih))
+            (λ b (hlt : m < b) (heq : succ n = succ b),
+              nat.no_confusion heq (λ (e : n = b),
+                acc.inv (eq.rec_on e ih) hlt)),
+        aux hlt rfl)))
+
+  definition not_lt_zero (a : nat) : ¬ a < zero :=
+  have aux : ∀ {b}, a < b → b = zero → false, from
+    λ b H, lt.cases_on H
+      (λ heq, nat.no_confusion heq)
+      (λ b h₁ heq, nat.no_confusion heq),
+  λ H, aux H rfl
+
+  definition zero_lt_succ (a : nat) : zero < succ a :=
+  rec_on a
+    (lt.base zero)
+    (λ a (hlt : zero < succ a), lt.step hlt)
+
+  definition lt.trans {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
+  have aux : ∀ {d}, d < c → b = d → a < b → a < c, from
+    (λ d H, lt.rec_on H
+      (λ h₁ h₂, lt.step (eq.rec_on h₁ h₂))
+      (λ 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 :=
+  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 :=
+  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 :=
+  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),
+  aux
+
+  definition lt.is_decidable_rel [instance] : decidable_rel lt :=
+  λ a b, rec_on b
+    (λ (a : nat), inr (not_lt_zero a))
+    (λ (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_neg : ¬ a < b₁,
+           have aux : ¬ succ a < succ b₁, from
+             λ h : succ a < succ b₁, h_neg (lt.cancel_succ_left_right 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_def_left {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)
+
+  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))
+
+  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))
+
+  definition lt.trichotomy (a b : nat) : a < b ∨ a = b ∨ b < a :=
+  rec_on b
+    (λa, cases_on a
+       (or.inr (or.inl rfl))
+       (λ a₁, or.inr (or.inr !zero_lt_succ)))
+    (λ 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, 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))))))
+    a
+
+  definition 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 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 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))
+
+  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 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_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_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_eq.trans {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 :=
+  eq.rec_on h₂ h₁
+
+  definition eq_lt.trans {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 :=
+  eq.rec_on (eq.rec_on h₁ rfl) h₂
+
+  calc_trans lt.trans
+  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
+
+  definition max (a b : nat) : nat :=
+  if a < b then b else a
+
+  definition min (a b : nat) : nat :=
+  if a < b then a else b
+
+  definition max_a_a (a : nat) : a = max a a :=
+  eq.rec_on !if_t_t rfl
+
+  definition max.eq_right {a b : nat} (H : a < b) : b = max a b :=
+  eq.rec_on (if_pos H) rfl
+
+  definition max.eq_left {a b : nat} (H : ¬ a < b) : a = max a b :=
+  eq.rec_on (if_neg 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 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)
+      (λ 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 (lt.asymm h),
+        eq.rec_on aux (le.of_lt h)))
+
+  definition gt a b := lt b a
+
+  notation a > b := gt a b
+
+  definition ge a b := le b a
+
+  notation a ≥ b := ge a b
+
+  definition add (a b : nat) : nat :=
+  rec_on b a (λ b₁ r, succ r)
+
+  notation a + b := add a b
+
+  definition sub (a b : nat) : nat :=
+  rec_on b a (λ b₁ r, pred r)
+
+  notation a - b := sub a b
+
+  definition mul (a b : nat) : nat :=
+  rec_on b zero (λ b₁ r, r + a)
+
+  notation a * b := mul a b
+end nat
diff --git a/library/data/nat/default.lean b/library/data/nat/default.lean
index 49532ac6f..89b96899f 100644
--- a/library/data/nat/default.lean
+++ b/library/data/nat/default.lean
@@ -2,4 +2,4 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 
-import .basic .order .sub .div .wf
+import .basic .order .sub .div
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 0c58520c6..3c1894ebd 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -11,7 +11,7 @@
 import logic .sub algebra.relation data.prod
 import tools.fake_simplifier
 
-open nat relation relation.iff_ops prod
+open relation relation.iff_ops prod
 open fake_simplifier decidable
 open eq.ops
 
@@ -87,7 +87,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_le.trans Hzx (lt_succ_imp_le H1)),
           have H2 : f' (succ m) x = rec_val x f, from
             calc
               f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
@@ -168,7 +168,7 @@ show lhs = rhs, from
      have H2b : ¬ x < y, from assume H, H1 (or.inr H),
       have ypos : y > 0, from ne_zero_imp_pos H2a,
       have xgey : x ≥ y, from not_lt_imp_ge H2b,
-      have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
+      have H4 : x - y < x, from sub_lt (lt_le.trans ypos xgey) ypos,
       calc
         lhs = succ (g1 (x - y)) : if_neg H1
           ... = succ (g2 (x - y)) : {H _ H4}
@@ -244,7 +244,7 @@ show lhs = rhs, from
       have H2b : ¬ x < y, from assume H, H1 (or.inr H),
       have ypos : y > 0, from ne_zero_imp_pos H2a,
       have xgey : x ≥ y, from not_lt_imp_ge H2b,
-      have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
+      have H4 : x - y < x, from sub_lt (lt_le.trans ypos xgey) ypos,
       calc
         lhs = g1 (x - y) : if_neg H1
           ... = g2 (x - y) : H _ H4
@@ -382,7 +382,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 le_lt.trans !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 :=
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 60b27f5f1..839e0844d 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -1,41 +1,52 @@
 --- Copyright (c) 2014 Floris van Doorn. All rights reserved.
 --- Released under Apache 2.0 license as described in the file LICENSE.
---- Author: Floris van Doorn
+--- Author: Floris van Doorn, Leonardo de Moura
 
 -- data.nat.order
 -- ==============
 --
 -- The ordering on the natural numbers
 
-import .basic logic.decidable
-import tools.fake_simplifier
+import .basic
 
-open nat eq.ops tactic
-open fake_simplifier
+open eq.ops
 
 namespace nat
 
-
 -- Less than or equal
 -- ------------------
 
-definition le (n m : ℕ) : Prop := exists k : nat, n + k = m
+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))
 
-notation a <= b := le a b
-notation a ≤ b  := le a b
+theorem le.add_right (n k : ℕ) : n ≤ n + k :=
+induction_on k
+  (calc n ≤ n        : le.refl n
+     ...  = n + zero : add.zero_right)
+  (λ k (ih : n ≤ n + k), calc
+     n   ≤ succ (n + k) : le.succ_right ih
+     ... = n + succ k   : add.succ_right)
 
-theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m :=
-exists_intro k H
+theorem le_intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
+h ▸ le.add_right n k
 
-theorem le_elim {n m : ℕ} (H : n ≤ m) : ∃k, n + k = m :=
-H
-
-irreducible le
+theorem le_elim {n m : ℕ} (h : n ≤ m) : ∃k, n + k = m :=
+le.rec_on h
+  (exists_intro 0 rfl)
+  (λ m (h : n < m), lt.rec_on h
+    (exists_intro 1 rfl)
+    (λ b hlt (ih : ∃ (k : ℕ), n + k = b),
+      obtain (k : ℕ) (h : n + k = b), from ih,
+      exists_intro (succ k) (calc
+        n + succ k = succ (n + k) : add.succ_right
+               ... = succ b       : h)))
 
 -- ### partial order (totality is part of less than)
 
 theorem le_refl (n : ℕ) : n ≤ n :=
-le_intro !add.zero_right
+le.refl n
 
 theorem zero_le (n : ℕ) : 0 ≤ n :=
 le_intro !add.zero_left
@@ -51,13 +62,7 @@ not_intro
     absurd H2 !succ_ne_zero)
 
 theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
-obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1,
-obtain (l2 : ℕ) (Hl2 : m + l2 = k), from le_elim H2,
-le_intro
-  (calc
-    n + (l1 + l2) =  n + l1 + l2 : !add.assoc⁻¹
-              ... = m + l2       : {Hl1}
-              ... = k            : Hl2)
+le.trans H1 H2
 
 theorem le_antisym {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
 obtain (k : ℕ) (Hk : n + k = m), from (le_elim H1),
@@ -218,7 +223,7 @@ theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m :=
 obtain (l : ℕ) (Hl : n + l = m), from (le_elim H),
 have H2 : k * n + k * l = k * m, from
   calc
-    k * n + k * l = k * (n + l) : by simp
+    k * n + k * l = k * (n + l) : mul.distr_left
               ... = k * m       : {Hl},
 le_intro H2
 
@@ -228,52 +233,14 @@ theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k :=
 theorem mul_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
 le_trans (mul_le_right H1 m) (mul_le_left H2 k)
 
--- mul_le_[left|right]_inv below
-
-definition le_decidable [instance] (n m : ℕ) : decidable (n ≤ m) :=
-have general : ∀n, decidable (n ≤ m), from
-  rec_on m
-    (take n,
-      rec_on n
-        (decidable.inl !le_refl)
-        (take m iH, decidable.inr !not_succ_zero_le))
-    (take (m' : ℕ) (iH1 : ∀n, decidable (n ≤ m')) (n : ℕ),
-      rec_on n
-        (decidable.inl !zero_le)
-        (take (n' : ℕ) (iH2 : decidable (n' ≤ succ m')),
-          decidable.by_cases
-            (assume Hp : n' ≤ m', decidable.inl (succ_le Hp))
-            (assume Hn : ¬ n' ≤ m',
-              have H : ¬ succ n' ≤ succ m', from
-                assume Hle : succ n' ≤ succ m',
-                  absurd (succ_le_cancel Hle) Hn,
-              decidable.inr H))),
-general n
-
 -- Less than, Greater than, Greater than or equal
 -- ----------------------------------------------
 
--- ge and gt will be transparent, so we don't need to reprove theorems for le and lt for them
-
-definition lt (n m : ℕ) := succ n ≤ m
-notation a < b := lt a b
-
-definition ge (n m : ℕ) := m ≤ n
-notation a >= b := ge a b
-notation a ≥ b := ge a b
-
-definition gt (n m : ℕ) := m < n
-notation a > b := gt a b
-
-theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := rfl
-
--- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2
-
 theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
-le_intro H
+le_succ_imp_lt (le_intro H)
 
 theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m :=
-le_elim H
+le_elim (lt_imp_le_succ H)
 
 theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
 lt_intro !add.move_succ
@@ -281,16 +248,18 @@ lt_intro !add.move_succ
 -- ### basic facts
 
 theorem lt_imp_ne {n m : ℕ} (H : n < m) : n ≠ m :=
-and.elim_right (succ_le_imp_le_and_ne H)
+λ heq : n = m, absurd H (heq ▸ !lt.irrefl)
 
 theorem lt_irrefl (n : ℕ) : ¬ n < n :=
 not_intro (assume H : n < n, absurd rfl (lt_imp_ne H))
 
-theorem succ_pos (n : ℕ) : 0 < succ n :=
-succ_le !zero_le
+theorem lt_def (n m : ℕ) : n < m ↔ succ n ≤ m :=
+iff.intro
+  (λ h, lt_imp_le_succ h)
+  (λ h, le_succ_imp_lt h)
 
-theorem not_lt_zero (n : ℕ) : ¬ n < 0 :=
-!not_succ_zero_le
+theorem succ_pos (n : ℕ) : 0 < succ n :=
+!zero_lt_succ
 
 theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
 discriminate
@@ -299,90 +268,53 @@ discriminate
 
 -- ### interaction with le
 
-theorem lt_imp_le_succ {n m : ℕ} (H : n < m) : succ n ≤ m :=
-H
-
-theorem le_succ_imp_lt {n m : ℕ} (H : succ n ≤ m) : n < m :=
-H
-
 theorem self_lt_succ (n : ℕ) : n < succ n :=
-!le_refl
+lt.base n
 
 theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m :=
-and.elim_left (succ_le_imp_le_and_ne H)
+le.of_lt H
 
 theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m :=
-le_imp_succ_le_or_eq H
+or.swap (le_def_right H)
 
 theorem le_ne_imp_lt {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : n < m :=
-le_ne_imp_succ_le H1 H2
-
-theorem le_imp_lt_succ {n m : ℕ} (H : n ≤ m) : n < succ m :=
-succ_le H
+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 H
-
--- ### transitivity, antisymmmetry
-
-theorem lt_le_trans {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k :=
-le_trans H1 H2
-
-theorem le_lt_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k :=
-le_trans (succ_le H1) H2
-
-theorem lt_trans {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k :=
-lt_le_trans H1 (lt_imp_le H2)
-
-theorem eq_le_trans {n m k : ℕ} (H1 : n = m) (H2 : m ≤ k) : n ≤ k :=
-H1⁻¹ ▸ H2
-
-theorem eq_lt_trans {n m k : ℕ} (H1 : n = m) (H2 : m < k) : n < k :=
-H1⁻¹ ▸ H2
-
-theorem le_eq_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m = k) : n ≤ k :=
-H2 ▸ H1
-
-theorem lt_eq_trans {n m k : ℕ} (H1 : n < m) (H2 : m = k) : n < k :=
-H2 ▸ H1
-
-calc_trans le_trans
-calc_trans lt_trans
-calc_trans lt_le_trans
-calc_trans le_lt_trans
-calc_trans eq_le_trans
-calc_trans eq_lt_trans
-calc_trans le_eq_trans
-calc_trans lt_eq_trans
+succ_le_cancel (lt_imp_le_succ H)
 
 theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m :=
-not_intro (assume H2 : m < n, absurd (le_lt_trans H H2) !lt_irrefl)
+le.rec_on H
+  !lt.irrefl
+  (λ 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_le.trans H H2) !lt_irrefl)
 
 theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n :=
-le_imp_not_gt (lt_imp_le H)
+lt.asymm H
+
+-- le_imp_not_gt (lt_imp_le H)
 
 -- ### interaction with addition
 
 theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
-!add.succ_right ▸ add_le_left H k
+le_succ_imp_lt (!add.succ_right ▸ add_le_left (lt_imp_le_succ 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)
+le_lt.trans (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_le.trans (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 :=
-add_le_cancel_left (!add.succ_right⁻¹ ▸ H)
+le_succ_imp_lt (add_le_cancel_left (!add.succ_right⁻¹ ▸ (lt_imp_le_succ 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)
@@ -395,43 +327,27 @@ theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m :=
 theorem succ_lt_cancel {n m : ℕ} (H : succ n < succ m) :  n < m :=
 add_lt_cancel_right (!add.one⁻¹ ▸ !add.one⁻¹ ▸ H)
 
-theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m
-:= lt_trans H !self_lt_succ
+theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m :=
+lt.step H
 
 -- ### totality of lt and le
 
 theorem le_or_gt {n m : ℕ} : n ≤ m ∨ n > m :=
-induction_on n
-  (or.inl !zero_le)
-  (take (k : ℕ),
-    assume IH : k ≤ m ∨ m < k,
-    or.elim IH
-      (assume H : k ≤ m,
-        obtain (l : ℕ) (Hl : k + l = m), from le_elim H,
-        discriminate
-          (assume H2 : l = 0,
-            have H3 : m = k,
-              from calc
-                m = k + l     : Hl⁻¹
-                  ... = k + 0 : {H2}
-                  ... = k     : !add.zero_right,
-            have H4 : m < succ k, from H3 ▸ !self_lt_succ,
-            or.inr H4)
-          (take l2 : ℕ,
-            assume H2 : l = succ l2,
-            have H3 : succ k + l2 = m,
-              from calc
-                succ k + l2 = k + succ l2 : !add.move_succ
-                        ... = k + l       : {H2⁻¹}
-                        ... = m           : Hl,
-            or.inl (le_intro H3)))
-      (assume H : m < k, or.inr (lt_imp_lt_succ H)))
+or.rec_on (lt.trichotomy n m)
+  (λ h : n < m, or.inl (le.of_lt h))
+  (λ h : n = m ∨ m < n, or.rec_on h
+    (λ h : n = m, eq.rec_on h (or.inl !le.refl))
+    (λ h : m < n, or.inr h))
 
 theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ n > m :=
-or.imp_or_left le_or_gt (assume H : n ≤ m, le_imp_lt_or_eq H)
+or.rec_on (lt.trichotomy n m)
+  (λ h, or.inl (or.inl h))
+  (λ h, or.rec_on h
+    (λ h, or.inl (or.inr h))
+    (λ h, or.inr h))
 
 theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ n > m :=
-iff.elim_left or.assoc !trichotomy_alt
+lt.trichotomy n m
 
 theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n :=
 or.imp_or_right le_or_gt (assume H : m < n, lt_imp_le H)
@@ -442,13 +358,6 @@ or.resolve_left le_or_gt H
 theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m :=
 or.resolve_right le_or_gt H
 
--- The following three theorems are automatically proved using the instance le_decidable
-definition lt_decidable [instance] (n m : ℕ) : decidable (n < m) := _
-definition gt_decidable [instance] (n m : ℕ) : decidable (n > m) := _
-definition ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m) := _
-
--- Note: interaction with multiplication under "positivity"
-
 -- ### misc
 
 protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
@@ -543,22 +452,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 H k,
-lt_le_trans H2 H3
+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
 
 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)
+le_lt.trans (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)
+le_lt.trans (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 (le_lt.trans !zero_le H1) H2,
+le_lt.trans H3 H4
 
 theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
 or.elim le_or_gt
@@ -571,7 +480,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 le_lt.trans 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
@@ -602,9 +511,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 H3)
+    show n = 1, from le_antisym H5 (lt_imp_le_succ H3))
   (assume H5 : n > 1,
-    have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
+    have H6 : n * m ≥ 2 * 1, from mul_le (lt_imp_le_succ H5) (lt_imp_le_succ 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 2db4608e7..ef06bb052 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -7,11 +7,10 @@
 --
 -- Subtraction on the natural numbers, as well as min, max, and distance.
 
-import data.nat.order
+import .order
 import tools.fake_simplifier
 
-open nat eq.ops tactic
-open helper_tactics
+open eq.ops
 open fake_simplifier
 
 namespace nat
@@ -19,12 +18,11 @@ namespace nat
 -- subtraction
 -- -----------
 
-definition sub (n m : ℕ) : nat := rec n (fun m x, pred x) m
-notation a - b := sub a b
+theorem sub_zero_right (n : ℕ) : n - 0 = n :=
+rfl
 
-theorem sub_zero_right (n : ℕ) : n - 0 = n
-
-theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)
+theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m) :=
+rfl
 
 irreducible sub
 
@@ -300,7 +298,7 @@ have xsuby_eq : x - y = x' - y', from calc
     ... = x' - y'           : !sub_succ_succ,
 have H1 : x' - y' ≤ x', from !sub_le_self,
 have H2 : x' < succ x', from !self_lt_succ,
-show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt_trans H1 H2
+show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt.trans H1 H2
 
 theorem sub_le_right {n m : ℕ} (H : n ≤ m) (k : nat) : n - k ≤ m - k :=
 obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
@@ -309,7 +307,7 @@ or.elim !le_total
   (assume H2 : k ≤ n,
     have H3 : n - k + l = m - k, from
       calc
-        n - k + l = l + (n - k) : by simp
+        n - k + l = l + (n - k) : add.comm
               ... = l + n - k   : (add_sub_assoc H2 l)⁻¹
               ... = n + l - k   : {!add.comm}
               ... = m - k       : {Hl},
@@ -324,10 +322,12 @@ sub_split
     have H3 : n ≤ k, from le_trans H (le_intro Hm),
     have H4 : m' + l + n = k - n + n, from
       calc
-        m' + l + n = n + l + m' : by simp
-               ... = m + m'     : {Hl}
-               ... = k          : Hm
-               ... = k - n + n  : (add_sub_ge_left H3)⁻¹,
+        m' + l + n = n + (m' + l) : add.comm
+               ... = n + (l + m') : add.comm
+               ... = n + l + m'   : add.assoc
+               ... = m + m'       : {Hl}
+               ... = k            : Hm
+               ... = k - n + n    : (add_sub_ge_left H3)⁻¹,
     le_intro (add.cancel_right H4))
 
 -- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m
@@ -352,9 +352,10 @@ sub_split
         assume Hkm : k + km = m,
         have H : k + (mn + km) = n, from
           calc
-            k + (mn + km) = k + km + mn : by simp
-                      ... = m + mn      : {Hkm}
-                      ... = n           : Hmn,
+            k + (mn + km) = k + (km + mn): add.comm
+                      ... = k + km + mn  : add.assoc
+                      ... = m + mn       : Hkm
+                      ... = n            : Hmn,
         have H2 : n - k = mn + km, from sub_intro H,
         H2 ▸ !le_refl))
 
@@ -362,24 +363,9 @@ sub_split
 -- add_rewrite sub_self mul_sub_distr_left mul_sub_distr_right
 
 
--- Max, min, iteration, and absolute difference
+-- absolute difference
 -- --------------------------------------------
 
-definition max (n m : ℕ) : ℕ := n + (m - n)
-definition min (n m : ℕ) : ℕ := m - (m - n)
-
-theorem max_le {n m : ℕ} (H : n ≤ m) : max n m = m :=
-add_sub_le H
-
-theorem max_ge {n m : ℕ} (H : n ≥ m) : max n m = n :=
-add_sub_ge H
-
-theorem left_le_max (n m : ℕ) : n ≤ max n m :=
-!le_add_sub_left
-
-theorem right_le_max (n m : ℕ) : m ≤ max n m :=
-!le_add_sub_right
-
 -- ### absolute difference
 
 -- This section is still incomplete
@@ -391,8 +377,9 @@ theorem dist_comm (n m : ℕ) : dist n m = dist m n :=
 
 theorem dist_self (n : ℕ) : dist n n = 0 :=
 calc
-  (n - n) + (n - n) = 0 + 0 : by simp
-                ... = 0     : by simp
+  (n - n) + (n - n) = 0 + (n - n) : sub_self
+                ... = 0 + 0       : sub_self
+                ... = 0           : rfl
 
 theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m :=
 have H2 : n - m = 0, from add.eq_zero_left H,
@@ -445,9 +432,10 @@ calc
 theorem dist_sub_move_add {n m : ℕ} (H : n ≥ m) (k : ℕ) : dist (n - m) k = dist n (k + m) :=
 have H2 : n - m + (k + m) = k + n, from
   calc
-    n - m + (k + m) = n - m + m + k : by simp
-                ... = n + k         : {add_sub_ge_left H}
-                ... = k + n         : by simp,
+    n - m + (k + m) = n - m + (m + k) : add.comm
+                ... = n - m + m + k   : add.assoc
+                ... = n + k           : {add_sub_ge_left H}
+                ... = k + n           : add.comm,
 dist_eq_intro H2
 
 theorem dist_sub_move_add' {k m : ℕ} (H : k ≥ m) (n : ℕ) : dist n (k - m) = dist (n + m) k :=
diff --git a/library/data/nat/wf.lean b/library/data/nat/wf.lean
deleted file mode 100644
index da2d8c32f..000000000
--- a/library/data/nat/wf.lean
+++ /dev/null
@@ -1,52 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-import data.nat.order logic.wf
-open nat eq.ops
-
-namespace nat
-
-inductive pred_rel : nat → nat → Prop :=
-intro : Π (n : nat), pred_rel n (succ n)
-
-definition not_pred_rel_zero (n : nat) : ¬ pred_rel n zero :=
-have aux : ∀{m}, pred_rel n m → succ n = m, from
-  λm H, pred_rel.rec_on H (take n, rfl),
-assume H : pred_rel n zero,
-  absurd (aux H) !succ_ne_zero
-
-definition pred_rel_succ {a b : nat} (H : pred_rel a (succ b)) : b = a :=
-have aux : pred (succ b) = a, from
-  pred_rel.rec_on H (λn, rfl),
-aux
-
--- Predecessor relation is well-founded
-definition pred_rel.wf : well_founded pred_rel :=
-well_founded.intro
-  (λn, induction_on n
-    (acc.intro zero (λy (H : pred_rel y zero), absurd H (not_pred_rel_zero y)))
-    (λa (iH : acc pred_rel a),
-       acc.intro (succ a) (λy (H : pred_rel y (succ a)),
-         have aux : a = y, from pred_rel_succ H,
-         eq.rec_on aux iH)))
-
--- Less-than relation is well-founded
-definition lt.wf [instance] : well_founded lt :=
-well_founded.intro
- (λn, induction_on n
-    (acc.intro zero (λ (y : nat) (H : y < 0),
-      absurd H !not_lt_zero))
-    (λ (n : nat) (iH : acc lt n),
-      acc.intro (succ n) (λ (m : nat) (H : m < succ n),
-        have H₁ : m < n ∨ m = n, from le_imp_lt_or_eq (succ_le_cancel (lt_imp_le_succ H)),
-        or.elim H₁
-          (assume Hlt : m < n, acc.inv iH Hlt)
-          (assume Heq : m = n, Heq⁻¹ ▸ iH))))
-
-definition measure {A : Type} (f : A → nat) : A → A → Prop :=
-inv_image lt f
-
-definition measure.wf {A : Type} (f : A → nat) : well_founded (measure f) :=
-inv_image.wf f lt.wf
-
-end nat
diff --git a/tests/lean/notation.lean b/tests/lean/notation.lean
index 4db3d71cd..e8789e886 100644
--- a/tests/lean/notation.lean
+++ b/tests/lean/notation.lean
@@ -1,4 +1,4 @@
-import logic data.nat.basic
+import logic data.num data.nat.basic
 open num
 constant b : num
 check b + b + b
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index 53d5baeb3..82bb730f7 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_le.trans 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 d6f28e025..2b3b71f9f 100644
--- a/tests/lean/run/div_wf.lean
+++ b/tests/lean/run/div_wf.lean
@@ -11,7 +11,7 @@ notation `dif` c `then` t:45 `else` e:45 := dite c t e
 -- Auxiliary lemma used to justify recursive call
 private lemma lt_aux {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
 have y0 : 0 < y, from and.elim_left H,
-have x0 : 0 < x, from lt_le_trans y0 (and.elim_right H),
+have x0 : 0 < x, from lt_le.trans y0 (and.elim_right H),
 sub_lt x0 y0
 
 definition wdiv.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
diff --git a/tests/lean/run/fib_wrec.lean b/tests/lean/run/fib_wrec.lean
index d46e6c262..dd6e6c78f 100644
--- a/tests/lean/run/fib_wrec.lean
+++ b/tests/lean/run/fib_wrec.lean
@@ -7,8 +7,8 @@ nat.cases_on n
   (λ (n₁ : nat), nat.cases_on n₁
     (λ (f : Π (m : nat), m < (succ zero) → nat), succ zero)
     (λ (n₂ : nat) (f : Π (m : nat), m < (succ (succ n₂)) → nat),
-       have l₁ : succ n₂ < succ (succ n₂), from self_lt_succ (succ n₂),
-       have l₂ : n₂ < succ (succ n₂), from lt_trans (self_lt_succ n₂) l₁,
+       have l₁ : succ n₂ < succ (succ n₂), from lt.base (succ n₂),
+       have l₂ : n₂ < succ (succ n₂), from lt.trans (lt.base n₂) l₁,
          f (succ n₂) l₁ + f n₂ l₂))
 
 definition fib (n : nat) :=
@@ -23,6 +23,8 @@ well_founded.fix_eq fib.F 1
 theorem fib.succ_succ_eq (n : nat) : fib (succ (succ n)) = fib (succ n) + fib n :=
 well_founded.fix_eq fib.F (succ (succ n))
 
-eval fib 5 -- ignores opaque annotations
-eval fib 6
-eval [strict] fib 5 -- take opaque/irreducible annotations into account
+example : fib 5 = 8 :=
+rfl
+
+example : fib 6 = 13 :=
+rfl
diff --git a/tests/lean/run/tree_height.lean b/tests/lean/run/tree_height.lean
index 950330d05..02f4b43fd 100644
--- a/tests/lean/run/tree_height.lean
+++ b/tests/lean/run/tree_height.lean
@@ -19,13 +19,13 @@ 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 (left_le_max (height t₁) (height t₂))
+le_imp_lt_succ (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 (right_le_max (height t₁) (height t₂))
+le_imp_lt_succ (max.right (height t₁) (height t₂))
 
 theorem height_lt.trans {A : Type} : transitive (@height_lt A) :=
-inv_image.trans lt height @lt_trans
+inv_image.trans lt height @lt.trans
 
 example : height_lt (leaf 2) (node (leaf 1) (leaf 2)) :=
 !height_lt.node_right
diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out
index 9f039f504..fc0090fcc 100644
--- a/tests/lean/whnf.lean.expected.out
+++ b/tests/lean/whnf.lean.expected.out
@@ -1,5 +1,5 @@
 whnf.lean:2:0: warning: imported file uses 'sorry'
-succ (nat.rec 2 (λ (n r : ℕ), succ r) zero)
+succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) zero)
 succ (succ (succ zero))
-succ (nat.rec a (λ (n r : ℕ), succ r) zero)
+succ (nat.rec a (λ (b₁ r : ℕ), succ r) zero)
 succ a