From 0e9a77cc53feab61a1f4c784f382908aad4b9821 Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Fri, 18 Dec 2020 23:34:58 +0000
Subject: [PATCH] feat(data/nat/basic): succ_lt_succ_iff (#5422)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
---
 src/data/nat/basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
index 7e6fa3f0f562f..338b272e0ceaa 100644
--- a/src/data/nat/basic.lean
+++ b/src/data/nat/basic.lean
@@ -265,6 +265,9 @@ by simp only [add_comm, add_one_le_iff]
 theorem of_le_succ {n m : ℕ} (H : n ≤ m.succ) : n ≤ m ∨ n = m.succ :=
 (lt_or_eq_of_le H).imp le_of_lt_succ id
 
+lemma succ_lt_succ_iff {m n : ℕ} : succ m < succ n ↔ m < n :=
+⟨lt_of_succ_lt_succ, succ_lt_succ⟩
+
 /-! ### `add` -/
 
 -- Sometimes a bare `nat.add` or similar appears as a consequence of unfolding