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