Remainder using truncate
ACL2 !>(rem 14 3)
ACL2 !>(rem -14 3)
ACL2 !>(rem 14 -3)
ACL2 !>(rem -14 -3)
ACL2 !>(rem -15 -3)
(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
(defun rem (x y)
(declare (xargs :guard (and (real/rationalp x)
(not (eql y 0)))))
(- x (* (truncate x y) y)))