Abstract
We demonstrate the existence and uniqueness of the base- representation of a natural number, where is any natural number greater than 1. This comes up when trying to translate mathematical contest problems and solutions into Isabelle/HOL.