Subtracting N-bit signeds creates 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.
You might ask, why have this rule when we have rules like basic-signed-byte-p-of-+? After all,
(defthm basic-signed-byte-p-of-binary-minus (implies (and (signed-byte-p n a) (signed-byte-p n b)) (signed-byte-p (+ 1 n) (- a b))))