import Mathlib.Data.PNat.Basic

/-!
# International Mathematical Olympiad 1977, Problem 6

Suppose `f : ℕ+ → ℕ+` satisfies `f(f(n)) < f(n + 1)` for all `n`.
Prove that `f(n) = n` for all `n`.
-/

namespace Imo1977P6

theorem imo1977_p6 (f : ℕ+ → ℕ+) (h : ∀ n, f (f n) < f (n + 1)) : ∀ n, f n = n := sorry

This problem has a complete solution written by Tian Chen.

The solution was imported from mathlib4/Archive/Imo/Imo1977Q6.lean.