Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2006P1

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Rat.Floor
public import Mathlib.Data.Rat.Star

public section


/-!
# USA Mathematical Olympiad 2006, Problem 1

Let p be a prime number and let s be an integer with 0 < s < p.
Prove that there exist integers m and n with 0 < m < n < p and

  {sm/p} < {sn/p} < s/p,

where {x} = x − ⌊x⌋ denotes the fractional part of x, if and only if
s is not a divisor of p − 1.
-/

namespace Usa2006P1

theorem usa2006_p1 (p s : ℕ) (hp : p.Prime) (hs0 : 0 < s) (hs1 : s < p) :
    (∃ m n : ℕ, 0 < m ∧ m < n ∧ n < p ∧
      Int.fract ((s : ℚ) * m / p) < Int.fract ((s : ℚ) * n / p) ∧
      Int.fract ((s : ℚ) * n / p) < (s : ℚ) / p) ↔
    ¬ s ∣ p - 1 := sorry

end Usa2006P1

File author(s): Kimi K3

This problem has a complete formalized solution.