From 16c23a20072d574ec812b6059978e3a78776c1ca Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 12 Apr 2024 08:39:24 +0200
Subject: Fix a proof

---
 backends/lean/Base/Primitives/Scalar.lean | 1 -
 1 file changed, 1 deletion(-)

(limited to 'backends')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index d1f7bee7..8de2b3f2 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -993,7 +993,6 @@ theorem core.num.checked_mul_spec {ty} {x y : Scalar ty} :
   simp only [checked_mul, Option.ofResult]
   have : Int.mul ↑x ↑y = ↑x * ↑y := by simp -- TODO: why do we need this??
   cases heq: x * y <;> simp_all <;> simp only [HMul.hMul, Scalar.mul, Mul.mul] at heq
-  <;> simp [add_neg_eq] at heq
   <;> simp_all
 
 theorem Scalar.div_equiv {ty} {x y : Scalar ty} :
-- 
cgit v1.2.3