norm_num
case neg.refine_2
p : ProblemPredicate (11 * 73)
h₁ : (digits 10 (11 * 73)).length = 3
h₂ : 73 = sumOfSquares (digits 10 (73 * 11))
H' : 73 = sumOfSquares (digits 10 (73 * 11)) → 73 = 50 ∨ 73 = 73
H : ∀ m < 73 * 11, ProblemPredicate m → SolutionPredicate m
l : 11 * 73 < 73 * 11 + 11
h : ¬11 * 73 < 73 * 11
⊢ 11 * 73 = 803
no goals