Compfiles: Catalog Of Math Problems Formalized In Lean

Russia1995P10

import Mathlib.Tactic
import Mathlib.Data.Nat.GCD.Basic

/-!
# Russian Mathematical Olympiad 1995, problem 10

Let m, n be positive integers such that

gcd(m, n) + lcm(m, n) = m + n.

Show that one of the two numbers is divisible by the other.
-/

namespace Russia1995P10

theorem russia1995_p10 {m n : ℕ} (h₀ : n ≠ 0 ∧ m ≠ 0)
  (h : gcd m n + lcm m n = m + n) :
  m ∣ n ∨ n ∣ m := sorry

end Russia1995P10

File author(s): Maximiliano Onofre Martínez

This problem has a complete formalized solution.