IMO 1977 Q6

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