`Compfiles/Imo1974P1.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1974, Problem 1

Three players $A, B$ and $C$ play the following game:

On each of three cards an integer is written.
These three numbers $p, q, r$ satisfy $0 < p < q < r$.
The three cards are shuffled and one is dealt to each player.
Each then receives the number of counters indicated by the card he holds.
Then the cards are shuffled again; the counters remain with the players.

This process (shuffling, dealing, giving out counters) takes place for at least two rounds. After the last round, $A$ has 20 counters in all, $B$ has 10 and $C$ has 9. At the last round $B$ received $r$ counters.

Who received $q$ counters on the first round?

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo1974P1.Player line 52 source
no axioms what this means
Proof uses: Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
determine Imo1974P1.solution line 54 source
standard axioms: propext what this means
Statement uses: Imo1974P1.Player
Proof uses: OfNat.ofNat, Nat
3 instances, coercions and auxiliary constants left out.
problem Imo1974P1.imo1974_p1 line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LT.lt, OfNat.ofNat, Equiv, Imo1974P1.Player, Fin, Eq, Finset.sum, Finset.range, Matrix.vecCons, Nat.succ, Matrix.vecEmpty, HSub.hSub, Imo1974P1.solution
Proof uses: LE.le, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true, eq_of_heq, List.Mem.tail, id, False.elim and 65 more
75 instances, coercions and auxiliary constants left out.
Tactic trace: 84 steps
Open to load the checked before-and-after goal states.