import Mathlib
/-!
# 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?
-/
namespace Imo1974P1
abbrev Player := Fin 3
/- determine -/ abbrev solution : Player := sorry -- player C
theorem imo1974_p1
(p q r : ℕ)
(hpqr : 0 < p ∧ p < q ∧ q < r)
(n : ℕ)
(hn : 1 < n)
(game : ℕ → (Player ≃ Fin 3))
(hA : ∑ k ∈ Finset.range n, ![p,q,r] (game k 0) = 20)
(hB : ∑ k ∈ Finset.range n, ![p,q,r] (game k 1) = 10)
(hC : ∑ k ∈ Finset.range n, ![p,q,r] (game k 2) = 9)
(hl : ![p,q,r] (game (n-1) 1) = r)
: game 0 solution = 1 := sorry
end Imo1974P1
This problem has a complete formalized solution.