Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1991P4

import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 1991, Problem 4
let $ a = \frac{m^{m+1} + n^{n+1}}{m^m + n^n} $ where $m$ and $n$ are positive integers. Prove that $a^m + a^n \geq m^m + n^n$.
-/

namespace Usa1991P4

theorem usa1991_p4 (m n : ℕ) (a: ℝ) (hm: 0 < m) (hn: 0 < n)
  (ha : a = (m^(m+1)+ n^(n+1))/(m^m + n^n)) : m^m + n^n ≤ a^m + a^n := sorry

end Usa1991P4

File author(s): Pacmanboss256, hillosanation

This problem has a complete formalized solution.