rw [List.replicate_add, Nat.ofDigits_append, Nat.ofDigits_append]
b m n : ℕ
⊢ Nat.ofDigits b (List.replicate (m + n) 1) =
    Nat.ofDigits b (List.replicate m 1) + Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
b m n : ℕ
⊢ Nat.ofDigits b (List.replicate m 1) + b ^ (List.replicate m 1).length * Nat.ofDigits b (List.replicate n 1) =
    Nat.ofDigits b (List.replicate m 1) +
      (Nat.ofDigits b (List.replicate m 0) + b ^ (List.replicate m 0).length * Nat.ofDigits b (List.replicate n 1))