## 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.

Open with the in-brower editor at live.lean-lang.org: