Function:
(defun rat-round-to-int$inline (rat rc) (declare (xargs :guard (and (rationalp rat) (natp rc)))) (rc-cases :rn (rat-round-to-int-rn rat) :rd (rat-round-to-int-rd rat) :ru (rat-round-to-int-ru rat) :rz (rat-round-to-int-rz rat) :other 0))
Theorem:
(defthm integerp-of-rat-round-to-int (b* ((r (rat-round-to-int$inline rat rc))) (integerp r)) :rule-classes :type-prescription)