Suppose, for a contradiction, that there are n people, each with a different number of friends. Since a person can't be friends with themselves, the numbers of friends is as follows:
0, 1, ..., n - 1
Then, the person with n - 1 friends has a friendship with everyone else in the group, including the person with 0 friends. But this is a contradiction! Thus there must be at least two people with the same number of friends.
Proof by contradiction is so much simpler than constructive proofs.
If yes, proof assistants have to be improved on conciseness, imho
“My wife and I greet 4 other couples. After the handshakes, I ask everyone how many people they shook hands with and get no duplicate replies; no one shook hands with their partner or themselves. How many people did my wife shake hands with?”
This puzzle stumps everyone I know that hasn’t been exposed to combinatorics.
We can easily see the 8-hand-shaker must have a 0-hand-shaker as their partner (since everyone else shook at least one hand, the all-shaker's). We can also see, when constructing possible graphs for smaller total numbers of couples (1, 2, 3, 4, etc.) that if the shake graph of N couples satisfies the uniqueness constraint then we can always add another couple in a way which preserves uniqueness: the new couple is an (2N-2, 0) shaker pair, where everyone else has their shake count incremented by one. Thus we see the question-asker's wife's shake-count is equal to the number of other couples, in this case 4.
I would still need to prove that any shake-graph satisfying the uniqueness constraint must be unique (under isomorphism swapping shake numbers within couples); we saw with the iterative construction that the answer is equal to the number of other couples, but it isn't yet clear that this is the only possible answer. Of course, we can infer from the question itself that there is a unique solution, and so any found solution must therefore be unique :P