diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
index 5064bd8307..dd714ec4d2 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
@@ -91,11 +91,6 @@ builtin_simproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
   let some v₂ ← Nat.fromExpr? e.appArg! | return .continue
   return .done { expr := toExpr (v₁ ^ v₂) }
 
-builtin_simproc [simp, seval] reduceAbs (natAbs _) := fun e => do
-  unless e.isAppOfArity ``natAbs 1 do return .continue
-  let some v ← fromExpr? e.appArg! | return .continue
-  return .done { expr := mkNatLit (natAbs v) }
-
 builtin_simproc [simp, seval] reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)
 builtin_simproc [simp, seval] reduceLE  (( _ : Int) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
 builtin_simproc [simp, seval] reduceGT  (( _ : Int) > _)  := reduceBinPred ``GT.gt 4 (. > .)
@@ -105,4 +100,12 @@ builtin_simproc [simp, seval] reduceNe  (( _ : Int) ≠ _)  := reduceBinPred ``N
 builtin_simproc [simp, seval] reduceBEq  (( _ : Int) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
 builtin_simproc [simp, seval] reduceBNe  (( _ : Int) != _)  := reduceBoolPred ``bne 4 (. != .)
 
+@[inline] def reduceNatCore (declName : Name) (op : Int → Nat) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName 1 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  return .done { expr := mkNatLit (op v) }
+
+builtin_simproc [simp, seval] reduceAbs (natAbs _) := reduceNatCore ``natAbs natAbs
+builtin_simproc [simp, seval] reduceToNat (Int.toNat _) := reduceNatCore ``Int.toNat Int.toNat
+
 end Int
diff --git a/tests/lean/run/simproc2.lean b/tests/lean/run/simproc2.lean
index ce1e357236..1052391976 100644
--- a/tests/lean/run/simproc2.lean
+++ b/tests/lean/run/simproc2.lean
@@ -10,3 +10,13 @@ example : foo x = 8 + 2 := by
   fail_if_success simp [-Nat.reduceAdd]
   simp only [Nat.reduceAdd]
   rw [foo]
+
+example (h : 0 = x) : (-2).toNat = x := by
+  simp
+  guard_target =ₛ 0 = x
+  assumption
+
+example (h : 1 = x) : (1 : Int).toNat = x := by
+  simp
+  guard_target =ₛ 1 = x
+  assumption