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>

archive/imo/imo1959_q1.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2020 Kevin Lacker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Lacker
+-/
+
+import tactic.ring
+
+open nat
+
+/-!
+# IMO 1959 Q1
+
+Prove that the fraction `(21n+4)/(14n+3)` is irreducible for every natural number `n`.
+
+Since Lean doesn't have a concept of "irreducible fractions" per se, we just formalize this
+as saying the numerator and denominator are relatively prime.
+-/
+
+lemma calculation (n k : ℕ) (h1 : k ∣ 21 * n + 4) (h2 : k ∣ 14 * n + 3) : k ∣ 1 :=
+have h3 : k ∣ 2 * (21 * n + 4), from dvd_mul_of_dvd_right h1 2,
+have h4 : k ∣ 3 * (14 * n + 3), from dvd_mul_of_dvd_right h2 3,
+have h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1, by ring,
+(nat.dvd_add_right h3).mp (h5 ▸ h4)
+
+theorem imo1959_q1 : ∀ n : ℕ, coprime (21 * n + 4) (14 * n + 3) :=
+assume n, coprime_of_dvd' (calculation n)