Multiplying constant N * N bit unsigneds creates an N+N bit unsigned.
This is a less general but more automatic lousy-unsigned-byte-p-of-* for reasoning about constant widths. The use of division here looks awful, but note the syntaxp hyp. This will let us get us things like:
(unsigned-byte-p 32 (* a b))
(defthm basic-unsigned-byte-p-of-* (implies (and (syntaxp (quotep n)) (natp n) (unsigned-byte-p (/ n 2) a) (unsigned-byte-p (/ n 2) b)) (unsigned-byte-p n (* a b))))