case inl
n b : ℕ
⊢ List.length (digits b 0) ≤ List.length (digits b (0 + 1))

case inr
n✝ b n : ℕ
hn : n ≠ 0
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
n✝ b n : ℕ
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
rcases Decidable.eq_or_ne n 0 with (rfl | hn)
case inr.inl
n✝ b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))

case inr.inr
n✝ b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
case inr
n✝ b n : ℕ
hn : n ≠ 0
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
cases' le_or_lt b 1 with hb hb
no goals
case inr.inr
n✝ b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
simpa [digits_len, hb, hn] using log_mono_right (le_succ _)
no goals
case inl
n b : ℕ
⊢ List.length (digits b 0) ≤ List.length (digits b (0 + 1))
simp
no goals
case inr.inl
n✝ b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
interval_cases b <;> simp_arith [digits_zero_succ', hn]