diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 413f165844..7ddcd7a540 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -152,12 +152,6 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
       bindErased decl.fvarId
       lowerCode k
     | some (.joinPoint ..) | none => panic! "unexpected value"
-  | .const ``Nat.succ _ args =>
-    let irArgs ← args.mapM lowerArg
-    let var ← bindVar decl.fvarId
-    let tmpVar ← newVar
-    let k := (.vdecl var .object (.fap ``Nat.add #[irArgs[0]!, (.var tmpVar)]) (← lowerCode k))
-    return .vdecl tmpVar .object (.lit (.num 1)) k
   | .const name _ args =>
     let irArgs ← args.mapM lowerArg
     if let some code ← tryIrDecl? name irArgs then
diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean
index 1f359b050b..a6105dadc5 100644
--- a/src/Lean/Compiler/LCNF/ToMono.lean
+++ b/src/Lean/Compiler/LCNF/ToMono.lean
@@ -92,6 +92,9 @@ partial def LetValue.toMono (e : LetValue) (resultFVar : FVarId) : ToMonoM LetVa
       return args[1]!.toLetValue
     else if declName == ``Quot.mk || declName == ``Quot.lcInv then
       return args[2]!.toLetValue
+    else if declName == ``Nat.succ then
+      -- This should have been handled in Code.toMono.
+      unreachable!
     else if let some (.ctorInfo ctorInfo) := (← getEnv).find? declName then
       if let some info ← hasTrivialStructure? ctorInfo.induct then
         args[ctorInfo.numParams + info.fieldIdx]!.toLetValue.toMono resultFVar
@@ -316,7 +319,15 @@ partial def trivialStructToMono (info : TrivialStructureInfo) (c : Cases) : ToMo
 
 partial def Code.toMono (code : Code) : ToMonoM Code := do
   match code with
-  | .let decl k => return code.updateLet! (← decl.toMono) (← k.toMono)
+  | .let decl k =>
+    match decl.value with
+    | .const ``Nat.succ _ args =>
+      let #[arg] := args | unreachable!
+      let oneDecl ← mkAuxLetDecl (.lit (.nat 1))
+      let decl ← decl.update decl.type (.const ``Nat.add [] #[arg, .fvar oneDecl.fvarId])
+      return .let oneDecl (.let decl (← k.toMono))
+    | _ =>
+      return code.updateLet! (← decl.toMono) (← k.toMono)
   | .fun decl k | .jp decl k => return code.updateFun! (← decl.toMono) (← k.toMono)
   | .unreach type => return .unreach (← toMonoType type)
   | .jmp fvarId args => return code.updateJmp! fvarId (← args.mapM argToMono)