Floor 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-floor.
(implies (and (signed-byte-p n a) (integerp b))
(equal (signed-byte-p n (floor a b))
(not (and (equal a (- (expt 2 (- n 1))))
(equal b -1))))))