IMO 1959 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem imo1959_q1.calculation (n k : ℕ) (h1 : k ∣ 21 * n + 4) (h2 : k ∣ 14 * n + 3) :

k ∣ 1

source

theorem imo1959_q1 (n : ℕ) :

(21 * n + 4).coprime (14 * n + 3)