Compfiles/Imo1996P6.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1996, Problem 6

Let p, q, n be three positive integers with p + q < n. Let (x₀, x₁, . . . , xₙ) be an (n + 1)-tuple of integers satisfying the following conditions: (a) x₀ = xₙ = 0. (b) For each i with 1 ≤ i ≤ n, either xᵢ − xᵢ₋₁ = p or xᵢ − xᵢ₋₁ = −q. Show that there exist indices i < j with (i, j) ≠ (0, n), such that xᵢ = xⱼ.

Imports (2)
Imported by 1 file
  1. lemma Imo1996P6.one_lt_gcd_of_not_coprime line 35 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Not, Nat.Coprime, Nat.gcd

    Proof uses: Iff.mpr, And, Ne, Nat.one_lt_iff_ne_zero_and_ne_one, And.intro, LT.lt.ne', Nat.gcd_pos_of_pos_left, of_eq_true, Eq, Eq.trans, False, True, congrArg, eq_false, id, not_false_eq_true

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma Imo1996P6.dist_gt_one_of_ne_sign line 38 source

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

    Statement uses: Int, Ne, Int.sign, OfNat.ofNat, LT.lt, abs, HSub.hSub

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma Imo1996P6.diff_ne_pm_one_of_dist_gt_one line 41 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, abs, HSub.hSub, And, Ne, Neg.neg

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. lemma Imo1996P6.ne_zero_of_eq_mul line 44 source

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

    Statement uses: Int, Ne, OfNat.ofNat, Eq, HMul.hMul, And

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. lemma Imo1996P6.sum_bivalued line 47 source

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

    Statement uses: Int, Finset, Nat, Membership.mem, Or, Eq, Exists, And, Finset.sum, HAdd.hAdd, HMul.hMul, HSub.hSub, Finset.card, LE.le

    Proof uses: Finset.filter, Exists.intro, SDiff.sdiff, Eq.mpr, Finset.disjUnion, Finset.disjoint_sdiff, id, congrArg, Eq.symm, Finset.sum_disjUnion, Eq.refl, Eq.mp, HSMul.hSMul, Finset.sum_const, Finset.sum_congr, rfl

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  6. problem Imo1996P6.imo1996_p6 line 63 source

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

    Statement uses: Nat, Int, LT.lt, OfNat.ofNat, HAdd.hAdd, Eq, Or, HSub.hSub, Neg.neg, Exists, And, LE.le, Ne, Prod, Prod.mk

    Proof uses: PSigma.mk, PSigma

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 263 steps (first 200 of 263)

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