import Mathlib.Tactic /-! # USA Mathematical Olympiad 1981, Problem 5 Show that for any positive real number x and any nonnegative integer n, ∑ₖ (⌊kx⌋/k) ≤ ⌊nx⌋ where the sum goes from k = 1 to k = n, inclusive. -/ namespace Usa1981P5 open BigOperators theorem usa1981_p5 (x : ℝ) (n : ℕ) : ∑ k in Finset.Icc 1 n, ((⌊k * x⌋:ℝ)/k) ≤ ⌊n * x⌋ := sorry

This problem has a complete solution written by David Renshaw.