Lemmas about signed-byte-p from the logops-lemmas book.
Theorem:
(defthm signed-byte-p-base-cases (and (equal (signed-byte-p size 0) (and (integerp size) (< 0 size))) (equal (signed-byte-p size -1) (and (integerp size) (< 0 size)))))
Theorem:
(defthm backchain-signed-byte-p-to-unsigned-byte-p (implies (and (syntaxp (constant-syntaxp size)) (< 0 size) (unsigned-byte-p (1- size) i)) (signed-byte-p size i)))