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