Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1977P6

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


end Imo1977P6

File author(s): Tian Chen

This problem has a complete formalized solution.

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