Compfiles/Imo1991P2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1991, Problem 2

Let n > 6 be an integer and a₁, a₂, ..., aₖ be all the natural numbers less than n and relatively prime to n. If

a₂ - a₁ = a₃ - a₂ = ... = aₖ - aₖ₋₁ > 0,

prove that n must either be a prime number of a power of 2.

Imports (2)
Imported by 1 file
  1. lemma Imo1991P2.aux line 36 source

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

    Statement uses: Nat, Odd, Ne, OfNat.ofNat, Eq, HMul.hMul, HPow.hPow, Nat.Coprime, HAdd.hAdd

    Proof uses: Odd.add_even, Iff.mpr, Even, And, Nat.even_pow, And.intro, even_two, Eq.mpr, id, congrArg, Nat.Coprime.mul_right, Nat.Coprime.pow_right, Odd.coprime_two_right, add_comm, propext, Nat.coprime_add_self_left, Nat.Coprime.pow_left, Odd.coprime_two_left

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  2. problem Imo1991P2.imo1991_p2 line 46 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Eq, Set, Set.ofPred, Exists, And, Nat.Coprime, HAdd.hAdd, Fin.mk, Or, Nat.Prime, Nat.isPowerOfTwo

    Proof uses: Iff, Membership.mem, Iff.mp, Set.ext_iff, Iff.mpr, And.intro, Nat.coprime_one_left, NeZero, NeZero.mk, LT.lt.ne', Fin.pos, HMul.hMul, Nat.recAux, Eq.mpr, id, congrArg, MulZeroClass.zero_mul, add_zero, Eq.refl, Eq.symm and 92 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 124 steps

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