have h3 : c ≠ 0 := by
  intro h4
  have h5 : (digits 10 c).length = 0 := by simp [h4]
  exact case_0_digit h5 h2
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
⊢ n ≥ 153846
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ n ≥ 153846