From c834b74772b7919d7f018aa419429ab292db9a7d Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Sun, 5 Jul 2026 06:33:55 -0500
Subject: [PATCH] =?UTF-8?q?fix:=20subleq=5Ffalls=5Fthrough=20=E2=80=94=20u?=
 =?UTF-8?q?se=20omega=20for=20=C2=AC(a=20=E2=89=A4=200)=20from=20a=20>=200?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

simp can't use h : a > 0 to rewrite if a ≤ 0. Added h_not_le by omega.

Build: 3301 jobs, 0 errors
---
 formal/SilverSight/Blitter6502OISC.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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) :