proposition 2 (division algorithm). For an integer \( a \) and a nonzero integer \( b \), there are unique integers \( q \) and \( r \) such that \( a = bq + r \) and \( 0 \le r < |b|. \)

Terminology:

• \( a \) is called the dividend.
• \( b \) is called the divisor.
• \( q \) is called the quotient.
• \( r \) is called the remainder.

Before proving the division algorithm, here are a few examples.

• Dividing \( 71 \) by \( 20 \) gives \( 71 = 20(3) + 11 \)
• Dividing \( 71 \) by \( -20 \) gives \( 71 = -20(-3) + 11 \)
• Dividing \( -71 \) by \( 20 \) gives \( -71 = 20(-4) + 9 \)
• Dividing \( -71 \) by \( -20 \) gives \( -71 = -20(4) + 9 \)

proof of division algorithm: If \( a \ge 0 \), consider the set \( S \), consisting of integers of the form \( a - bn \) where \( n \) is an integer, ie, \[ S = { a - bn: n \in \mathbf{Z} }. \] The intersection of \( S \) the with nonnegative integers is non-empty, since \( a \) itself is nonnegative. By the well-ordering principle, there must be a unique smallest nonnegative element of \( S \), say \( r = a - bq \). Since \( r - |b| \) is a smaller element of \( S \), it must be negative, hence \( r < |b| \).

If \( a < 0 \), then \( -a \) is positive, which was proven above to be expressable as \( -a = bQ + R. \) If \( R = 0 \), set \( q = -Q \) and \( r = 0. \) Otherwise, set \( r = -R + |b| \) and \( q = -Q - |b| / b. \) In either case, we have \[ a = -bQ - R = bq + r \] with \( 0 \le r < |b|. \)

in code

In most programming languages, the implementation of a division and remainder (modulus) operator likely will not match the specification given by the division algorithm: when the dividend or divisor is negative, it may result in a negative remainder.

In ruby, for example, integer division is floor division, so the quotient a / b is computed by rounding down the rational number \( a / b \). Therefore, the sign of the remainder a % b is the same as the sign of the divisor b.

In rust, on the other hand, integer division is truncation, so the quotient a / b is computed by rounding the rational number \( a / b \) toward zero. Therefore, the sign of the remainder a % b is the same as the sign of the dividend a.

  def test_div_rem
    test_inputs(:include_zero => false).each do |(a, b)|
      quo, rem = div_rem(a, b)

      assert 0 <= rem
      assert rem < b.abs
      assert_equal a, b*quo + rem
    end
  end

def div_rem(a, b)
  rem = a % b
  rem += b.abs if rem < 0
  quo = (a - rem) / b

  [quo, rem]
end