Function:
(defun imod$inline (i j) (declare (xargs :guard (and (integerp i) (and (integerp j) (not (= 0 j)))))) (let ((__function__ 'imod)) (declare (ignorable __function__)) (mbe :logic (mod (ifix i) (ifix j)) :exec (mod i j))))
Theorem:
(defthm imod-type (b* ((int (imod$inline i j))) (integerp int)) :rule-classes :type-prescription)