feat(archive/imo): formalize IMO 1964 problem 1 (#4935)
This is an alternative approach to #4369, where progress seems to have stalled. I avoid integers completely by working with `nat.modeq`, and deal with the cases of n mod 3 by simply breaking into three cases.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
