==> induction/party.p <==
You're at a party. Any two (different) people at the party have exactly one
friend in common (the friend is also at the party). Prove that there is at
least one person at the party who is a friend of everyone else. Assume that
the friendship relation is symmetric and not reflexive.