Major Section: ACL2-BUILT-INS
Example Forms: (nonnegative-integer-quotient 14 3) ; equals 4 (nonnegative-integer-quotient 15 3) ; equals 5
(nonnegative-integer-quotient i j) returns the integer quotient
of the integers i and (non-zero) j, i.e., the largest k
such that (* j k) is less than or equal to i. Also
see floor, see ceiling and see truncate, which are
derived from this function and apply to rational numbers.
The guard of (nonnegative-integer-quotient i j) requires that
i is a nonnegative integer and j is a positive integer.
To see the ACL2 definition of this function, see pf.
