IMO 2011 Q5

Let f be a function from the set of integers to the set of positive integers. Suppose that, for any two integers m and n, the difference f(m) - f(n) is divisible by f(m - n). Prove that, for all integers m and n with f(m) ≤ f(n), the number f(n) is divisible by f(m).

theorem imo2011_q5 (f : ℤ → ℤ) (hpos : ∀ (n : ℤ), 0 < f n) (hdvd : ∀ (m n : ℤ), f (m - n) ∣ f m - f n) (m : ℤ) (n : ℤ) : f m ≤ f n → f m ∣ f n