### NONNEGATIVE-INTEGER-QUOTIENT

natural number division function
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.