Isabelle/HOL中是否存在通用Base-n整数表示标准理论？

我正尝试将数学竞赛问题转化为Isabelle/HOL形式，这类问题常涉及诸如“某数在7进制下的最后两位是什么？”的提问。Isabelle/HOL在ThreeDivides理论中对十进制整数表示有基础处理，Num理论中有更详尽的二进制数字表示理论，基础nat数据类型可视为一进制表示，但我尚未找到处理通用Base-n表示的理论文件。

我需要的理论需包含以下内容：

• 表示的存在性与唯一性定理（ThreeDivides并未为其十进制表示证明该定理）
• 便捷的写法支持（如[4, 3]⇘base 5⇙ = 23）
• 基础操作规则

我可自行创建该理论文件，但希望避免重复劳动，故询问：Isabelle/HOL中是否有用于陈述和证明任意自然数进制下整数数位相关事实的标准理论？

内容的提问来源于stack exchange，提问作者Charles Staats