IMO 1977 Q6 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We first prove the problem statement for f : ℕ → ℕ then we use it to prove the statement for positive naturals.

theorem imo1977_q6.imo1977_q6_nat (f : ℕ → ℕ) (h : ∀ (n : ℕ), f (f n) < f (n + 1)) (n : ℕ) :

f n = n

theorem imo1977_q6 (f : ℕ+ → ℕ+) (h : ∀ (n : ℕ+), f (f n) < f (n + 1)) (n : ℕ+) :

f n = n