Update SSA/Projects/InstCombine/ForLean.lean

Co-authored-by: Tobias Grosser <[email protected]>
opencompl · Sep 26, 2024 · 3fa90d0 · 3fa90d0
1 parent ca7b0c3
commit 3fa90d0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -622,7 +622,7 @@ theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} (n : Nat) :
   simp [← BitVec.shiftLeft_or_distrib]
 
 @[simp]
-theorem neg_eq_sub_zero (x : BitVec w) : - x = 0 - x := by
+theorem zero_sub (x : BitVec w) : 0 - x = - x = := by
     simp [bv_toNat]
 
 end BitVec