Compfiles/Imo1975P2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1975, Problem 2

Let a1 < a2 < a3 < ... be positive integers. Prove that for every i >= 1, there are infinitely many a_n that can be written in the form a_n = ra_i + sa_j, with r, s positive integers and j > i.

Imports (5)
Imported by 1 file
  1. problem Imo1975P2.imo1975_p2 line 32 source

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

    Statement uses: Nat, Int, LT.lt, OfNat.ofNat, HAdd.hAdd, Exists, And, LE.le, Eq, HMul.hMul

    Proof uses: Int.natAbs, Ne, Ne.symm, Int.ne_of_lt, GT.gt, Dvd.dvd, HSub.hSub, Classical.byContradiction, Not, Nat.succ, Finset.sup, List.toFinset, List.range, GE.ge, Finset.le_sup, Eq.mpr, Membership.mem, Finset, List, id and 83 more

    119 instances, coercions and auxiliary constants left out.

    Tactic trace: 76 steps

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