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.