@[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 {b n : Nat} (h : n < b) : b.toDigits n = [n.digitChar]

@[simp]

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)

theorem Nat.toDigits_of_base_le {b n : Nat} (hb : 1 < b) (h : b ≤ n) : b.toDigits n = b.toDigits (n / b) ++ [(n % b).digitChar]

theorem Nat.toDigits_eq_if {b n : Nat} (hb : 1 < b) : b.toDigits n = if n < b then [n.digitChar] else b.toDigits (n / b) ++ [(n % b).digitChar]

theorem Nat.length_toDigits_pos {b n : Nat} : 0 < (b.toDigits n).length

theorem Nat.length_toDigits_le_iff {b n k : Nat} (hb : 1 < b) (h : 0 < k) : (b.toDigits n).length ≤ k ↔ n < b ^ k

theorem Nat.repr_eq_ofList_toDigits {n : Nat} : n.repr = String.ofList (toDigits 10 n)

theorem Nat.toString_eq_ofList_toDigits {n : Nat} : toString n = String.ofList (toDigits 10 n)

@[simp]

theorem Nat.toString_eq_repr {n : Nat} : toString n = n.repr

@[simp]

theorem Nat.reprPrec_eq_repr {n i : Nat} : reprPrec n i = Std.Format.text n.repr

@[simp]

theorem Nat.repr_eq_repr {n : Nat} : repr n = Std.Format.text n.repr

theorem Nat.repr_of_lt {n : Nat} (h : n < 10) : n.repr = String.singleton n.digitChar

theorem Nat.repr_of_ge {n : Nat} (h : 10 ≤ n) : n.repr = (n / 10).repr ++ String.singleton (n % 10).digitChar

theorem Nat.repr_eq_repr_append_repr {n : Nat} (h : 10 ≤ n) : n.repr = (n / 10).repr ++ (n % 10).repr

theorem Nat.length_repr_pos {n : Nat} : 0 < n.repr.length

theorem Nat.length_repr_le_iff {n k : Nat} (h : 0 < k) : n.repr.length ≤ k ↔ n < 10 ^ k