Solving a puzzle using the Isabelle proof assistant

A machine checked proof of the following: "In a finite group of people, some of whom are friends with some of the others there must be at least two people who have the same number of friends."