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.