have h1 : Nat.digits b x ≠ [] :=
  Nat.digits_ne_nil_iff_ne_zero.mpr (Nat.pos_iff_ne_zero.mp xpos)
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
⊢ (b.digits x).prod ≤ x
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).prod ≤ x