obtain ⟨rfl, H⟩ := H
c n : ℕ
H : SearchUpTo c n
H' : c = sumOfSquares (digits 10 n) → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
⊢ SearchUpTo (c + 1) (c * 11 + 11)