import Mathlib.Data.Set.Card
/-!
# International Mathematical Olympiad 1966, Problem 1.
In a mathematical contest, three problems, A, B, C were posed. Among the
participants there were 25 students who solved at least one problem each.
Of all the contestants who did not solve problem A, the number who solved
B was twice the number who solved C. The number of students who solved
only problem A was one more than the number of students who solved A
and at least one other problem. Of all students who solved just one problem,
half did not solve problem A. How many students solved only problem B?
-/
namespace Imo1966P1
variable {U : Type*} [DecidableEq U]
/- determine -/ abbrev solution : ℕ := sorry
theorem imo1966_p1 (A B C : Finset U)
(h1 : (A ∪ B ∪ C).card = 25)
(h2 : (B \ A).card = 2 * (C \ A).card)
(h3 : ((A \ B) \ C).card = 1 + (A ∩ (B ∪ C)).card)
(h4 : ((A \ B) \ C).card = ((B \ A) \ C).card + ((C \ A) \ B).card) :
((B \ A) \ C).card = solution := sorry
end Imo1966P1
This problem has a complete formalized solution.