Commit 2020-11-15 04:56 9dd9b6b0
View on Github →refactor(archive/imo/imo1969_q1): prove infinite
statement, cleanup (#4391)
The previous formalization didn't quite prove that there were infinitely many natural numbers with the desired property, but rather that for any natural number there's a larger one with the property. This PR changes the ending to prove that the set of integers described in the problem statement is infinite
.