		Search-engine friendly clone of the ACL2 documentation.

Nonnegative-integer-quotient

Natural number division function

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.

Function: nonnegative-integer-quotient

(defun nonnegative-integer-quotient (i j)
  (declare (xargs :guard (and (integerp i)
                              (not (< i 0))
                              (integerp j)
                              (< 0 j))))
  (if (or (= (nfix j) 0) (< (ifix i) j))
      0
    (+ 1
       (nonnegative-integer-quotient (- i j)
                                     j))))