have hmb : 0 < m * b := lt_mul_of_lt_of_one_lt' hm hb
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)