From 6b36076ab57f692acf086f4d8ab0ff7bc2ff9201 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 15 Jun 2015 21:38:41 +1000
Subject: [PATCH] feat({library,hott}/init/nat): add sub_le_succ

---
 hott/init/nat.hlean   | 1 +
 library/init/nat.lean | 1 +
 2 files changed, 2 insertions(+)

diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index d15e72ed0..d5b719010 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -287,4 +287,5 @@ namespace nat
     (le.refl a)
     (λ b₁ ih, le.trans !pred_le ih)
 
+  lemma sub_lt_succ (a b : ℕ) : a - b < succ a := lt_succ_of_le (sub_le a b)
 end nat
diff --git a/library/init/nat.lean b/library/init/nat.lean
index a3ff98e02..83cec94fa 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -286,4 +286,5 @@ namespace nat
     (le.refl a)
     (λ b₁ ih, le.trans !pred_le ih)
 
+  lemma sub_lt_succ (a b : ℕ) : a - b < succ a := lt_succ_of_le (sub_le a b)
 end nat