import Mathlib.Tactic
/-!
# International Mathematical Olympiad 1995, Problem 6
Let p be an odd prime number. How many p-element subsets A of
{1, 2, ..., 2p} are there, the sum of whose elements is
divisible by p?
-/
namespace Imo1995P6
/- determine -/ abbrev solution (p : ℕ) : ℕ := sorry
theorem imo1995_p6 (p : ℕ) (hp : p.Prime) (hodd : Odd p) :
(((Finset.Icc 1 (2 * p)).powersetCard p).filter
(fun A ↦ p ∣ ∑ x ∈ A, x)).card = solution p := sorry
end Imo1995P6
This problem does not yet have a complete formalized solution.