exact Nat.le_add_left _ _
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤
    (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯
no goals