1.3 Euclidean division
For all \(n, d\),
\[ n = (n \mathbin {/} d) \cdot d + n \bmod d. \]
\((n \bmod d {\lt} d) \iff (0 {\lt} d)\).
If \(m {\lt} d\) then \(m \mathbin {/} d = 0\).
\((p \cdot q + r) \bmod p = r \bmod p\).
For \(0 {\lt} p\),
\[ (p \cdot q + r) \mathbin {/} p = q + r \mathbin {/} p. \]