module
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Analysis.Normed.Ring.Lemmas
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Rat.Star
public import Mathlib.RingTheory.Coprime.Lemmas
public import Mathlib.Tactic.IntervalCases
public section
/-!
# International Mathematical Olympiad 1967, Problem 6
In a sports contest, there were m medals awarded on n successive days (n > 1).
On the first day, one medal and 1/7 of the remaining (m − 1) medals were awarded.
On the second day, two medals and 1/7 of the now remaining medals were awarded;
and so on. On the n-th and last day, the remaining n medals were awarded.
How many days did the contest last, and how many medals were awarded altogether?
-/
namespace Imo1967P6
/-- The process described in the problem, from the point of view of the medals
remaining: `r k` is the number of medals left at the start of day `k + 1`
(so `r 0 = m`). On day `k` (for `1 ≤ k ≤ n - 1`), `k` medals and one seventh
of the rest are awarded, which has to be a whole number of medals. On the last
day the remaining `n` medals are awarded, i.e. `r (n - 1) = n`. -/
abbrev MedalsProcess (m n : ℕ) (r : ℕ → ℤ) : Prop :=
r 0 = ↑m ∧ r (n - 1) = ↑n ∧
∀ k, 1 ≤ k → k ≤ n - 1 →
7 ∣ r (k - 1) - ↑k ∧ r k = r (k - 1) - (↑k + (r (k - 1) - ↑k) / 7)
/- determine -/ abbrev solution : ℕ × ℕ := sorry
theorem imo1967_p6 (m n : ℕ) (hn : 1 < n) :
(∃ r : ℕ → ℤ, MedalsProcess m n r) ↔ (m, n) = solution := sorry
end Imo1967P6
This problem has a complete formalized solution.