import Mathlib.Data.Real.Basic
import Mathlib.Tactic
/-!
# International Mathematical Olympiad 2005, Problem 3
Let `x`, `y` and `z` be positive real numbers such that `xyz ≥ 1`. Prove that:
`(x^5 - x^2)/(x^5 + y^2 + z^2) + (y^5 - y^2)/(y^5 + z^2 + x^2) + (z^5 - z^2)/(z^5 + x^2 + y^2) ≥ 0`
-/
namespace Imo2005P3
theorem imo2005_p3 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x * y * z ≥ 1) :
(x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) + (y ^ 5 - y ^ 2) / (y ^ 5 + z ^ 2 + x ^ 2) +
(z ^ 5 - z ^ 2) / (z ^ 5 + x ^ 2 + y ^ 2) ≥
0 := sorry
end Imo2005P3
This problem has a complete formalized solution.
The solution was imported from mathlib4/Archive/Imo/Imo2005P3.lean.