chore: proof of bitvec_290__292 (#601)

PR solving [issue 598](#598) --------- Co-authored-by: Tobias Grosser <[email protected]>
opencompl · Sep 8, 2024 · a938776 · a938776
1 parent a9c1590
commit a938776
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -523,6 +523,11 @@ theorem two_mul {x : BitVec w} :
   rw [ssr]
   omega
 
+@[simp]
+theorem one_shiftLeft_mul {x y : BitVec w} :
+    1#w <<< x.toNat * y = y <<< x.toNat := by
+  simp [←BitVec.mul_twoPow_eq_shiftLeft, BitVec.mul_comm]
+
 end BitVec
 
 namespace Bool