Multiplying N * N bit signeds creates an N+N bit signed.
This is a powerful rule with a nice statement, but it rarely unifies with anything automatically. See also basic-signed-byte-p-of-* and also see lousy-signed-byte-p-of-mixed-*.
Theorem:
(defthm lousy-signed-byte-p-of-* (implies (and (signed-byte-p n a) (signed-byte-p n b)) (signed-byte-p (+ n n) (* a b))))