def tb.sb8

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:489

import Base

489def tb.sb8(+x: Nat) -> {x == Nat.sub(Nat.add(8n, x), 8n) : Nat}:
490  match x:
491    case 0n:
492      {==}
493    case 1n+p:
494      {==}