import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2023, Problem 3

For each integer k ≥ 2, determine all infinite sequences of positive
integers a₁, a₂, ... for which there exists a polynomial P of the form

  P(x) = xᵏ + cₖ₋₁xᵏ⁻¹ + ... + c₁x + c₀,

where c₀, c₁, ..., cₖ₋₁ are non-negative integers, such that

  P(aₙ) = aₙ₊₁aₙ₊₂⋯aₙ₊ₖ

for every integer n ≥ 1.
-/

namespace Imo2023P3

open BigOperators

/- determine -/ abbrev solution_set {k : ℕ} (hk : 2 ≤ k) : Set (ℕ+ → ℕ+) := sorry

theorem imo2023_p3 {k : ℕ} (hk : 2 ≤ k) (a : ℕ+ → ℕ+) :
    a ∈ solution_set hk ↔
    (∃ c : Fin (k+1) → ℕ+, c k = 1 ∧ ∀ n, (hn : 0 < n) →
      ∏ j : Fin k, a ⟨n + j.val + 1, Nat.succ_pos _⟩ =
      ∑ j : Fin (k + 1), ((a ⟨n, hn⟩).val)^j.val * c j) := sorry

This problem does not yet have a complete solution.