@[simp]

theorem Nat.isDigit_digitChar {n : Nat} : n.digitChar.isDigit = decide (n < 10)

theorem Nat.isDigit_of_mem_toDigits {b n : Nat} {c : Char} (hb₁ : 0 < b) (hb₂ : b ≤ 10) (hc : c ∈ b.toDigits n) : c.isDigit = true

theorem Nat.toDigits_of_lt_base {n b : Nat} (h : n < b) : b.toDigits n = [n.digitChar]

theorem Nat.toDigits_zero (b : Nat) : b.toDigits 0 = ['0']

theorem Nat.toDigits_append_toDigits {b n d : Nat} (hb : 1 < b) (hn : 0 < n) (hd : d < b) : b.toDigits n ++ b.toDigits d = b.toDigits (b * n + d)