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-*.
(implies (and (signed-byte-p n a)
(signed-byte-p n b))
(signed-byte-p (+ n n) (* a b))))