have h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
⊢ False
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False