refactor(library): move nat lemmas to library/init/data/nat/lemmas.lean

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
 

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
 

library/data/nat/default.lean

@@ -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

library/data/nat/order.lean

@@ -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

library/data/nat/sub.lean

@@ -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

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,