feat(library/data/nat): add more basic theorems for definitional package

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

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