diff --git a/formal/SilverSight/Blitter6502OISC.lean b/formal/SilverSight/Blitter6502OISC.lean
index e278e3ab..f647232d 100644
--- a/formal/SilverSight/Blitter6502OISC.lean
+++ b/formal/SilverSight/Blitter6502OISC.lean
@@ -138,7 +138,8 @@ theorem subleq_falls_through (s : M6502State) (inst : SUBLEQ)
     (h : s.mem inst.dstB.addr - s.mem inst.srcA.addr > 0) :
     (execSUBLEQ s inst).pc = s.pc + 3 := by
   unfold execSUBLEQ
-  simp [h]
+  have h_not_le : ¬ (s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0) := by omega
+  simp [h_not_le]
 
 /-- Blitter step count: 3 SUBLEQ instructions per byte. -/
 theorem blitter_step_count (prog : BlitterProgram) :