Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1989P6

import Mathlib.Tactic
import Mathlib.Data.Nat.Dist

/-!
# International Mathematical Olympiad 1989, Problem 6

A permutation $\{x_1, \ldots, x_{2n}\}$ of the set $\{1,2, \ldots, 2n\}$ where $n$ is a positive integer,
is said to have property $T$ if $|x_i - x_{i + 1}| = n$ for at least one $i \in \{1,2, \ldots, 2n - 1\}$.
Show that, for each $n$, there are more permutations with property $T$ than without.
-/

namespace Imo1989P6

open Equiv

variable (n : ℕ)

def T (x : Perm (Finset.Icc 1 (2*n))) :=
  ∃ i, ∃ _ : i ∈ Finset.Icc 1 (2*n-1),
    (x ⟨i, by grind⟩ : ℕ).dist (x ⟨i+1, by grind⟩) = n


theorem imo1989_p6 (npos : 0 < n) : {x | T n x}.ncard > {x | ¬ T n x}.ncard := sorry


end Imo1989P6

File author(s): Constantin Seebach

This problem has a complete formalized solution.