import Mathlib.Tactic
/-!
# USA Mathematical Olympiad 1993, Problem 3
Consider functions f : [0,1] → ℝ which satisfy
(i) f(x) ≥ 0 for all x ∈ [0,1]
(ii) f(1) = 1
(iii) f(x) + f(y) ≤ f (x + y) whenever x, y and x + y are all in [0,1].
Determine the smallest constant c such that
f(x) ≤ cx
for every function satisfying (i) - (iii) and every x ∈ [0,1].
-/
namespace Usa1993P3
def valid (f : Set.Icc 0 1 → ℝ) : Prop :=
(∀ x, 0 ≤ f x) ∧
f 1 = 1 ∧
∀ x y, (h : x.val + y.val ∈ Set.Icc 0 1) → f x + f y ≤ f ⟨x.val + y.val, h⟩
/- determine -/ abbrev min_c : ℝ := sorry
theorem usa1993_p5 :
IsLeast {c | ∀ f, valid f ∧ ∀ x, f x ≤ c * x } min_c := sorry
end Usa1993P3
This problem does not yet have a complete formalized solution.