feat(archive/imo): formalize IMO 1959 problem 1 (#4340)
This is a formalization of the problem and solution for the first problem on the 1959 IMO:
Prove that the fraction (21n+4)/(14n+3) is irreducible for every natural number n.
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
