Commit 2020-11-12 23:23 6b3a2d1d

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.