diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
index 8993b82b84..f201698022 100644
--- a/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
+++ b/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
@@ -17,13 +17,14 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   else if c₂.isValid then
     let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
     return some (mkConst ``True, p)
-  else if c₁ != c₂ then
-    let c₂ : LinearCnstr := c₂.toExpr
-    let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
-    let r ← c₂.toArith ctx
-    return some (r, p)
   else
-    return none
+    let c₂ : LinearCnstr := c₂.toExpr
+    let r ← c₂.toArith ctx
+    if r != e then
+      let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
+      return some (r, p)
+    else
+      return none
 
 def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   if let some arg := e.not? then