Theorem: Imo1960P1.searchUpTo_end (Compfiles/Imo1960P1.lean)

State before:
c : ℕ
H : SearchUpTo c 1001
n : ℕ
ppn : ProblemPredicate n
⊢ n < 1001
Tactic:
linarith [lt_1000 ppn]
State after:
no goals