feat(data/nat/basic): some lemmas (#792)

* feat(data/nat/basic): some lemmas

* fixing namespace, moving lemma

Author: kim-em

src/data/nat/basic.lean

@@ -40,6 +40,16 @@ by rw [← sub_one, nat.sub_sub, one_add]; refl
 
 lemma pred_eq_sub_one (n : ℕ) : pred n = n - 1 := rfl
 
+lemma one_le_of_lt {n m : ℕ} (h : n < m) : 1 ≤ m :=
+lt_of_le_of_lt (nat.zero_le _) h
+
+lemma le_pred_of_lt {n m : ℕ} (h : m < n) : m ≤ n - 1 :=
+nat.sub_le_sub_right h 1
+
+/-- This ensures that `simp` succeeds on `pred (n + 1) = n`. -/
+@[simp] lemma pred_one_add (n : ℕ) : pred (1 + n) = n :=
+by rw [add_comm, add_one, pred_succ]
+
 theorem pos_iff_ne_zero : n > 0 ↔ n ≠ 0 :=
 ⟨ne_of_gt, nat.pos_of_ne_zero⟩
 
@@ -75,6 +85,9 @@ by rw [add_comm, nat.sub_add_cancel h]
 protected theorem sub_eq_of_eq_add (h : k = m + n) : k - m = n :=
 begin rw [h, nat.add_sub_cancel_left] end
 
+lemma sub_sub_sub_cancel_right {a b c : ℕ} (h₂ : c ≤ b) : (a - c) - (b - c) = a - b :=
+by rw [nat.sub_sub, ←nat.add_sub_assoc h₂, nat.add_sub_cancel_left]
+
 theorem sub_min (n m : ℕ) : n - min n m = n - m :=
 nat.sub_eq_of_eq_add $ by rw [add_comm, sub_add_min]