mathlib3 documentation

mathlib-archive / imo.imo2011_q5

IMO 2011 Q5 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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