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