mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
5 lines
319 B
Text
5 lines
319 B
Text
import Mathlib.Tactic.Omega
|
|
|
|
theorem test (omega : Int) (h_omega : omega ≥ 0) (h_bound : 65536 + omega ≤ 2147483647) :
|
|
(if (65536 + omega).toNat % 4294967296 < 2147483648 then Int.ofNat ((65536 + omega).toNat % 4294967296) else Int.ofNat ((65536 + omega).toNat % 4294967296) - 4294967296) ≥ 65536 := by
|
|
omega
|