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