diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
index f9f2c07776..23c0d1b90b 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -275,7 +275,7 @@ def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step :
       applySimprocConst (mkConst ``True) ``Nat.Simproc.le_add_le #[x, yb, yo, leProof]
     else
       let finExpr := mkLENat (toExpr (xn - yn)) yb
-      let geProof ← mkOfDecideEqTrue (mkGENat yo x)
+      let geProof ← mkOfDecideEqTrue (mkGENat x yo)
       applySimprocConst finExpr ``Nat.Simproc.le_add_ge #[x, yb, yo, geProof]
   | .offset xb xo xn, .offset yb yo yn => do
     if xn ≤ yn then
diff --git a/tests/lean/run/simproc1.lean b/tests/lean/run/simproc1.lean
index 647b841975..37db98df71 100644
--- a/tests/lean/run/simproc1.lean
+++ b/tests/lean/run/simproc1.lean
@@ -32,3 +32,5 @@ example : x + foo 2 = 12 + x := by
   -- We can use `-` to disable `simproc`s
   fail_if_success simp [-reduce_foo]
   simp_arith
+
+example (x : Nat) (h : x < 86) : ¬100 ≤ x + 14 := by simp; exact h