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

The N+1 is needed in case of the minimum integer.

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-2 and basic-signed-byte-p-of-binary-minus.

**Theorem: **

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