Function:
(defun rat-round-to-int-rz (rat) (declare (xargs :guard (rationalp rat))) (let ((__function__ 'rat-round-to-int-rz)) (declare (ignorable __function__)) (truncate rat 1)))
Theorem:
(defthm integerp-of-rat-round-to-int-rz (b* ((r (rat-round-to-int-rz rat))) (integerp r)) :rule-classes :type-prescription)