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