diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
index db9dff719b..d4131e497c 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
@@ -12,6 +12,7 @@ open Lean Meta Simp
 macro "declare_uint_simprocs" typeName:ident : command =>
 let ofNat := typeName.getId ++ `ofNat
 let ofNatCore := mkIdent (typeName.getId ++ `ofNatCore)
+let ofNatLT := mkIdent (typeName.getId ++ `ofNatLT)
 let toNat := mkIdent (typeName.getId ++ `toNat)
 let fromExpr := mkIdent `fromExpr
 `(
@@ -60,6 +61,12 @@ builtin_dsimproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _
   let value := $(mkIdent ofNat) value
   return .done <| toExpr value
 
+builtin_dsimproc [simp, seval] $(mkIdent `reduceOfNatLT):ident ($ofNatLT _ _) := fun e => do
+  unless e.isAppOfArity $(quote ofNatLT.getId) 2 do return .continue
+  let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let value := $(mkIdent ofNat) value
+  return .done <| toExpr value
+
 builtin_dsimproc [simp, seval] $(mkIdent `reduceOfNat):ident ($(mkIdent ofNat) _) := fun e => do
   unless e.isAppOfArity $(quote ofNat) 1 do return .continue
   let some value ← Nat.fromExpr? e.appArg! | return .continue
diff --git a/tests/lean/simprocEval3.lean b/tests/lean/simprocEval3.lean
index dac5568317..37db04f803 100644
--- a/tests/lean/simprocEval3.lean
+++ b/tests/lean/simprocEval3.lean
@@ -10,6 +10,11 @@ example (h : x = 8) : x = UInt32.ofNatCore 8 (by decide) := by
   trace_state
   assumption
 
+example (h : x = 8) : x = UInt32.ofNatLT 8 (by decide) := by
+  simp
+  trace_state
+  assumption
+
 example : foo x = 8 + 2 := by
   simp
   trace_state
diff --git a/tests/lean/simprocEval3.lean.expected.out b/tests/lean/simprocEval3.lean.expected.out
index 3dd108b02a..d10fc3ca82 100644
--- a/tests/lean/simprocEval3.lean.expected.out
+++ b/tests/lean/simprocEval3.lean.expected.out
@@ -4,6 +4,9 @@ h : x = 8
 x : UInt32
 h : x = 8
 ⊢ x = 8
+x : UInt32
+h : x = 8
+⊢ x = 8
 x : Nat
 ⊢ foo x = 10
 x : Nat