import Mathlib.Tactic /-! # International Mathematical Olympiad 1974, Problem 5 What are the possible values of a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) as a,b,c,d range over the positive real numbers? -/ namespace Imo1974P5 /- determine -/ abbrev solution_set : Set ℝ := sorry theorem imo1974_p5 (s : ℝ) : s ∈ solution_set ↔ ∃ a b c d : ℝ, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) := sorry

This problem has a complete solution written by David Renshaw.