2.2 The carry predicate
For a base \(p\), position \(i\), and natural numbers \(a, b\), define
\[ \mathrm{carry}(p, i, a, b) \; :=\; [p^i \leq (a \bmod p^i) + (b \bmod p^i)]. \]
This is \(1\) (true) when adding \(a\) and \(b\) produces a carry at position \(i\) in base \(p\).
For \(p {\gt} 0\) and \(k \leq n\),
\[ \left\lfloor \frac{n}{p^i} \right\rfloor = \left\lfloor \frac{k}{p^i} \right\rfloor + \left\lfloor \frac{n-k}{p^i} \right\rfloor + \mathrm{carry}(p, i, k, n-k). \]
Proof. Write \(n = k + (n-k)\) and apply Lemma 2.1 with \(m = p^i\).