6.1 Digit extraction
For \(p \geq 2\), the \(i\)-th digit of \(n\) in base \(p\) is
\[ d_i(n) := \left\lfloor \frac{n}{p^i} \right\rfloor \bmod p. \]
For \(p \geq 2\),
\[ d_i(n) {\lt} p. \]
Proof.
For \(p \geq 2\) and \(n {\gt} 0\),
\[ n = \sum _{i=0}^{\texttt{trunc\_ log}(p,n)} d_i(n) \cdot p^i. \]
Proof.