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.
(defthm basic-signed-byte-p-of-unary-minus (implies (signed-byte-p n x) (signed-byte-p (+ 1 n) (- x))))