From 9d0fe5cbf92bc69d6a1833544965802b2209e5da Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Oct 2021 16:37:58 -0700
Subject: [PATCH] chore: add simp rule `Nat.lt x y = (x < y)`

---
 src/Init/Data/Nat/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index dd9205c92a..e49a40a613 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -47,6 +47,9 @@ namespace Nat
 @[simp] theorem add_eq : Nat.add x y = x + y :=
   rfl
 
+@[simp] theorem lt_eq : Nat.lt x y = (x < y) :=
+  rfl
+
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n
   | 0   => rfl
   | n+1 => congrArg succ (Nat.zero_add n)