Negative N-bit unsigned is an N+1 bit signed.

ACL2's fancy unification stuff means this works fine in the common case that you're dealing with quoted constants for N and N+1. See also basic-signed-byte-p-of-unary-minus and basic-signed-byte-p-of-binary-minus.

**Theorem: **

(defthm basic-signed-byte-p-of-unary-minus-2 (implies (unsigned-byte-p n x) (signed-byte-p (+ 1 n) (- x))))