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.

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

theorem imo1959_q1 (n : ℕ) : (21 * n + 4).Coprime (14 * n + 3)