Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2005P2

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2005, Problem 2

Let $a_1, a_2, \dots$ be a sequence of integers with infinitely many positive and negative terms.
Suppose that for every positive integer $n$ the numbers $a_1, a_2, \dots, a_n$ leave $n$ different remainders upon division by $n$.
Prove that every integer occurs exactly once in the sequence.
-/

namespace Imo2005P2



theorem imo2005_p2 (a : ℕ → ℤ)
  (pos_inf : Set.Infinite {i | 0 < a i})
  (neg_inf : Set.Infinite {i | a i < 0})
  (rem : ∀ n > 0, ((Finset.range n).image (fun i => a i % n)).card = n)
    : ∀ z : ℤ, ∃! i, a i = z := sorry


end Imo2005P2

File author(s): Constantin Seebach

This problem has a complete formalized solution.