Rem is a Common Lisp function. See any Common Lisp documentation
for more information.
truncate
Major Section: PROGRAMMING
ACL2 !>(rem 14 3) 2 ACL2 !>(rem -14 3) -2 ACL2 !>(rem 14 -3) 2 ACL2 !>(rem -14 -3) -2 ACL2 !>(rem -15 -3) 0 ACL2 !>
(Rem i j) is that number k for which (* j (truncate i j)) added
to k equals i.
The guard for (rem i j) requires that i and j are rational
(real, in ACL2(r)) numbers and j is non-zero.
Rem is a Common Lisp function. See any Common Lisp documentation
for more information.