Compfiles/Imo2011P5.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2011, Problem 5

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).

Imports (2)
Imported by 1 file
  1. problem Imo2011P5.imo2011_p5 line 29 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Int, LT.lt, OfNat.ofNat, Dvd.dvd, HSub.hSub, LE.le

    Proof uses: Trans.trans, Eq, rfl, Eq.mpr, id, congrArg, sub_zero, Eq.refl, Iff.mp, Int.dvd_iff_dvd_of_dvd_sub, dvd_refl, Neg.neg, zero_sub, HAdd.hAdd, sub_neg_eq_add, zero_add, le_of_lt, Int.dvd_antisymm, dite, And and 69 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

    Open to load the checked before-and-after goal states.