case succ.succ
n m b : ℕ
⊢ m < succ (succ b) ^ List.length (digits (succ (succ b)) m)
n b m : ℕ
hb : 1 < b
⊢ m < b ^ List.length (digits b m)
rcases b with (_ | _ | b) <;> try simp_all
no goals
case succ.succ
n m b : ℕ
⊢ m < succ (succ b) ^ List.length (digits (succ (succ b)) m)
exact lt_base_pow_length_digits'
case succ.succ
n m b : ℕ
⊢ m < succ (succ b) ^ List.length (digits (succ (succ b)) m)
case succ.succ
n m b : ℕ
hb : 1 < succ (succ b)
⊢ m < succ (succ b) ^ List.length (digits (succ (succ b)) m)
simp_all