Documentation

Archive.Imo.Imo2011Q5

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 nf m f n