case succ.succ
n m b : ℕ
⊢ ¬m = 0 → succ (succ b) ^ List.length (digits (succ (succ b)) m) ≤ succ (succ b) * m
n b m : ℕ
hb : 1 < b
⊢ m ≠ 0 → b ^ List.length (digits b m) ≤ b * m
rcases b with (_ | _ | b) <;> try simp_all
no goals
case succ.succ
n m b : ℕ
⊢ ¬m = 0 → succ (succ b) ^ List.length (digits (succ (succ b)) m) ≤ succ (succ b) * m
exact base_pow_length_digits_le' b m
case succ.succ
n m b : ℕ
⊢ ¬m = 0 → succ (succ b) ^ List.length (digits (succ (succ b)) m) ≤ succ (succ b) * m
case succ.succ
n m b : ℕ
hb : 1 < succ (succ b)
⊢ m ≠ 0 → succ (succ b) ^ List.length (digits (succ (succ b)) m) ≤ succ (succ b) * m
simp_all