Compfiles/Imo1994P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathmatical Olympiad 1994, Problem 1

Let m and n be two positive integers. Let a₁, a₂, ..., aₘ be m different numbers from the set {1, 2, ..., n} such that for any two indices i and j with 1 ≤ i ≤ j ≤ m and aᵢ + aⱼ ≤ n, there exists an index k such that aᵢ + aⱼ = aₖ. Show that (a₁+a₂+...+aₘ)/m ≥ (n+1)/2

Imports (7)
Imported by 1 file
  1. theorem Imo1994P1.tedious line 49 source

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

    Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Eq, HSub.hSub, HMod.hMod

    Proof uses: LT.lt, Exists, Fin.mk, Eq.mp, LE.le, congrArg, propext, le_iff_exists_add, Nat.succ, Nat.lt_succ_iff, Eq.mpr, id, Fin.val_mk, Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.add_sub_cancel, Eq.refl, Eq.symm

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  2. problem Imo1994P1.imo1994_p1 line 59 source

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

    Statement uses: Nat, Finset, Eq, Finset.card, HAdd.hAdd, OfNat.ofNat, Membership.mem, And, LT.lt, LE.le, HMul.hMul, Finset.sum

    Proof uses: OrderEmbedding, Fin, Finset.orderEmbOfFin, Finset.orderEmbOfFin_mem, Equiv, Equiv.subLeft, Fin.last, Finset.univ, Eq.mpr, Finset.image, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Set, id, congrArg, propext and 107 more

    157 instances, coercions and auxiliary constants left out.

    Tactic trace: 34 steps

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