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