From 21b16fd97c350e23f5b16263a582e2429b391fbf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 Nov 2014 13:11:16 -0800
Subject: [PATCH] feat(library/data/nat): add more basic theorems for
 definitional package

---
 library/data/nat/decl.lean | 10 ++++++++++
 library/data/nat/sub.lean  |  5 -----
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/library/data/nat/decl.lean b/library/data/nat/decl.lean
index a01108bce..bfc3f0925 100644
--- a/library/data/nat/decl.lean
+++ b/library/data/nat/decl.lean
@@ -314,4 +314,14 @@ namespace nat
             (lt.trans (@ih b₁ bpos) (lt.base a₁)))),
   λ h₁ h₂, aux h₁ h₂
 
+  definition sub_pred (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 :=
+  induction_on b
+    (le.refl a)
+    (λ b₁ ih, le.trans !sub_pred ih)
+
 end nat
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 06b758f85..1624b43c5 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -222,11 +222,6 @@ or.elim !le_total
   (assume H3 : n ≤ m, (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 H3))
   (assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3))
 
-theorem sub_le_self (n m : ℕ) : n - m ≤ n :=
-sub_split
-  (assume H : n ≤ m, !zero_le)
-  (take k : ℕ, assume H : m + k = n, le_intro (!add.comm ▸ H))
-
 theorem le_elim_sub {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
 obtain (k : ℕ) (Hk : n + k = m), from le_elim H,
 exists_intro k