case succ.succ
n m d b : ℕ
hd : d ∈ digits (succ (succ b)) m
⊢ d < succ (succ b)
n b m d : ℕ
hb : 1 < b
hd : d ∈ digits b m
⊢ d < b
rcases b with (_ | _ | b) <;> try simp_all
no goals
case succ.succ
n m d b : ℕ
hd : d ∈ digits (succ (succ b)) m
⊢ d < succ (succ b)
exact digits_lt_base' hd
case succ.succ
n m d b : ℕ
hd : d ∈ digits (succ (succ b)) m
⊢ d < succ (succ b)
case succ.succ
n m d b : ℕ
hb : 1 < succ (succ b)
hd : d ∈ digits (succ (succ b)) m
⊢ d < succ (succ b)
simp_all