have h5 : (digits 10 c).length = 0 := by simp [h4]
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h4 : c = 0
⊢ False
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h4 : c = 0
h5 : (digits 10 c).length = 0
⊢ False