Kummer’s theorem in MathComp

2.1 The floor-division addition identity

Lemma 2.1 Floor-division addition identity

Let \(m {\gt} 0\). Then for all \(a, b \in \mathbb {N}\),

\[ \left\lfloor \frac{a+b}{m} \right\rfloor = \left\lfloor \frac{a}{m} \right\rfloor + \left\lfloor \frac{b}{m} \right\rfloor + [m \leq (a \bmod m) + (b \bmod m)] \]

where \([\cdot ]\) denotes the Iverson bracket. Proof. Write \(a = qm + r\) and \(b = q'm + r'\) with \(0 \leq r, r' {\lt} m\). Then \(a + b = (q + q')m + (r + r')\). Since \(0 \leq r + r' {\lt} 2m\), we have \(\lfloor (r+r')/m\rfloor \in \{ 0, 1\} \), and it equals \(1\) exactly when \(r + r' \geq m\).

Lemma 2.2 Modular addition

For \(m {\gt} 0\),

\[ (a + b) \bmod m = ((a \bmod m) + (b \bmod m)) \bmod m. \]

Proof.

Lemma 2.3 Sum of remainders bound

For \(m {\gt} 0\),

\[ (a \bmod m) + (b \bmod m) {\lt} 2m. \]

Proof.

Lemma 2.4 Division of sum of remainders

For \(m {\gt} 0\),

\[ \left\lfloor \frac{(a \bmod m) + (b \bmod m)}{m} \right\rfloor \leq 1. \]

Proof.

Lemma 2.5 Carry is a boolean division

For \(m {\gt} 0\),

\[ [m \leq (a \bmod m) + (b \bmod m)] = \left\lfloor \frac{(a \bmod m) + (b \bmod m)}{m} \right\rfloor . \]

(The right-hand side is \(0\) or \(1\).) Proof.