Truncate of an N-bit signed by an integer is usually an
N-bit signed. (Strong form, case splitting, disabled by default).
See also basic-signed-byte-p-of-truncate, which we leave
(implies (and (signed-byte-p n a) (integerp b))
(equal (signed-byte-p n (truncate a b))
(not (and (equal a (- (expt 2 (- n 1))))
(equal b -1))))))