Compfiles/Imo1984P2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1984, Problem 2

Find a pair of positive integers a and b such that

(i) ab(a + b) is not divisible by 7. (ii) (a + b)⁷ - a⁷ - b⁷ is divisible by 7⁷.

Imports (2)
Imported by 1 file
  1. determine Imo1984P2.a line 28 source

    no axioms what this means

    Statement uses: Int

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  2. determine Imo1984P2.b line 29 source

    no axioms what this means

    Statement uses: Int

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  3. problem Imo1984P2.imo1984_p2 line 31 source

    standard axioms: propext what this means

    Statement uses: And, LT.lt, Int, OfNat.ofNat, Imo1984P2.a, Imo1984P2.b, Not, Dvd.dvd, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub

    Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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