case h.e'_3
n b m : ℕ
⊢ m = ofDigits (b + 2) (digits (b + 2) m)
n b m : ℕ
⊢ m < (b + 2) ^ List.length (digits (b + 2) m)
convert @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'
no goals
case h.e'_3
n b m : ℕ
⊢ m = ofDigits (b + 2) (digits (b + 2) m)
rw [ofDigits_digits (b + 2) m]