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,

See also basic-signed-byte-p-of-unary-minus and basic-signed-byte-p-of-unary-minus-2.

**Theorem: **

(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))))