Compfiles/Usa1998P5.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1998, Problem 5

Prove that for each n ≥ 2, there is a set S of n integers such that (a-b)² divides ab for every distinct a,b ∈ S.

Imports (2)
Imported by 1 file
  1. problem Usa1998P5.usa1998_p5 line 26 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Finset, Int, And, Eq, Finset.card, Membership.mem, Ne, Dvd.dvd, HPow.hPow, HSub.hSub, HMul.hMul

    Proof uses: Nat.recAux, Exists.intro, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congr, congrArg, forall_congr, False, implies_congr, Eq.refl, implies_true, eq_self, Not, and_self, HAdd.hAdd, Finset.prod, Finset.erase, LT.lt and 68 more

    139 instances, coercions and auxiliary constants left out.

    Tactic trace: 66 steps

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