Built-in axioms and theorems about random$.
Theorem:
(defthm natp-random$ (natp (car (random$ n state))) :rule-classes :type-prescription)
Theorem:
(defthm random$-linear (and (<= 0 (car (random$ n state))) (implies (posp n) (< (car (random$ n state)) n))) :rule-classes :linear)