From 97b98c58d01e028d8d4d591df7210eb1e062bec7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Jan 2017 17:39:37 -0800
Subject: [PATCH] refactor(library): move nat lemmas to
 library/init/data/nat/lemmas.lean

---
 library/data/list/basic.lean      |  1 -
 library/data/list/comb.lean       |  1 -
 library/data/nat/default.lean     |  9 ---------
 library/data/nat/order.lean       | 19 -------------------
 library/data/nat/sub.lean         | 18 ------------------
 library/init/data/nat/lemmas.lean | 10 ++++++++++
 6 files changed, 10 insertions(+), 48 deletions(-)
 delete mode 100644 library/data/nat/default.lean
 delete mode 100644 library/data/nat/order.lean
 delete mode 100644 library/data/nat/sub.lean

diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index bcd9ac8951..e3050f276e 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -6,7 +6,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn
 Basic properties of lists.
 -/
 import init.data.list.basic
-import data.nat.order
 
 universe variables u v w
 
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index c5c9be34ed..33331756b6 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura, Haitao Zhang, Floris van Doorn
 List combinators.
 -/
 import init.data.list.basic
-import data.nat.order
 
 universe variables u v w
 
diff --git a/library/data/nat/default.lean b/library/data/nat/default.lean
deleted file mode 100644
index c7e48f5f82..0000000000
--- a/library/data/nat/default.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Jeremy Avigad
-
-This is a minimal port of functions from the lean2 library.
--/
-
-import data.nat.order .sub
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
deleted file mode 100644
index 79a6b9740e..0000000000
--- a/library/data/nat/order.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
-
-The order relation on the natural numbers.
-
-This is a minimal port of functions from the lean2 library.
--/
-
-namespace nat
-
-/- min -/
-
-theorem zero_min (a : ℕ) : min 0 a = 0 := min_eq_left (zero_le a)
-
-theorem min_zero (a : ℕ) : min a 0 = 0 := min_eq_right (zero_le a)
-
-end nat
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
deleted file mode 100644
index 75cd63d2ad..0000000000
--- a/library/data/nat/sub.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-/-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Authors: Floris van Doorn, Jeremy Avigad
-Subtraction on the natural numbers, as well as min, max, and distance.
--/
-
-namespace nat
-
-/- subtraction -/
-
--- defined in data/nat/sub.lean
-protected theorem sub_le_sub_right {n m : ℕ} (H : n ≤ m) : Πk, n - k ≤ m - k
-| 0 := H
-| (succ z) := pred_le_pred (sub_le_sub_right z)
-
-end nat
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index 97270240bd..959bc7ba2f 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -415,6 +415,10 @@ lt_succ_of_le (sub_le a b)
 lemma sub_lt_succ_iff_true (a b : ℕ) : a - b < succ a ↔ true :=
 iff_true_intro (sub_lt_succ a b)
 
+protected theorem sub_le_sub_right {n m : ℕ} (h : n ≤ m) : ∀ k, n - k ≤ m - k
+| 0        := h
+| (succ z) := pred_le_pred (sub_le_sub_right z)
+
 /- bit0/bit1 properties -/
 
 protected lemma bit0_succ_eq (n : ℕ) : bit0 (succ n) = succ (succ (bit0 n)) :=
@@ -683,6 +687,12 @@ min_eq_left (zero_le a)
 lemma min_zero_right (a : ℕ) : min a 0 = 0 :=
 min_eq_right (zero_le a)
 
+theorem zero_min (a : ℕ) : min 0 a = 0 :=
+min_zero_left a
+
+theorem min_zero (a : ℕ) : min a 0 = 0 :=
+min_zero_right a
+
 -- Distribute succ over min
 lemma min_succ_succ (x y : ℕ) : min (succ x) (succ y) = succ (min x y) :=
 have f : x ≤ y → min (succ x) (succ y) = succ (min x y), from λp,