Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1985P2

import Mathlib.Algebra.Order.Ring.Canonical
import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Data.Int.NatAbs
import Mathlib.Data.Nat.ModEq

/-!
# International Mathematical Olympiad 1985, Problem 5

Fix a natural number $n ≥ 3$ and define $N=\{1, 2, 3, \dots, n-1\}$.
Fix another natural number $j ∈ N$ coprime to $n$. Each number in
$N$ is now colored with one of two colors, say red or black, so that:

1. $i$ and $n-i$ always receive the same color, and
2. $i$ and $|j-i|$ receive the same color for all $i ∈ N, i ≠ j$.

Prove that all numbers in $N$ must receive the same color.
-/

namespace Imo1985P2

/-- The conditions on the problem's coloring `C`.
Although its domain is all of `ℕ`, we only care about its values in `Set.Ico 1 n`. -/
def Condition (n j : ℕ) (C : ℕ → Fin 2) : Prop :=
  (∀ i ∈ Set.Ico 1 n, C i = C (n - i)) ∧
  ∀ i ∈ Set.Ico 1 n, i ≠ j → C i = C (j - i : ℤ).natAbs

theorem imo1985_p2 {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n)
    (cpj : Nat.Coprime n j) {C : ℕ → Fin 2} (hC : Condition n j C)
    {i : ℕ} (hi : i ∈ Set.Ico 1 n) :
    C i = C j := sorry

end Imo1985P2

File author(s): Jeremy Tan

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo1985Q2.lean.