rw [←List.dropLast_append_getLast h1, List.prod_append, List.prod_singleton]
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).prod ≤ x
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x