Multiplying constant N * N bit signeds creates an N+N bit signed.
This is a less general but more automatic version of lousy-signed-byte-p-of-*. It's good for constant widths.
The use of division here looks awful, but note the syntaxp
hyp: we'll only do these divisions when we know
See also basic-signed-byte-p-of-mixed-*.
(defthm basic-signed-byte-p-of-* (implies (and (syntaxp (quotep n)) (natp n) (signed-byte-p (/ n 2) a) (signed-byte-p (/ n 2) b)) (signed-byte-p n (* a b))))