have h4 : List.mapIdx (fun i a => a * b ^ i) (Nat.digits b x) ≠ [] :=
  List.mapIdx_eq_nil.not.mpr h1
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x