omega
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : ¬11 * m < c * 11
⊢ m = c
no goals