IMO 1977 Q6 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
f : ℕ+ → ℕ+ satisfies
f(f(n)) < f(n + 1) for all
f(n) = n for all
We first prove the problem statement for
f : ℕ → ℕ
then we use it to prove the statement for positive naturals.