clear h7
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) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (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)).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) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x