jmoy

section ‹A Simple Graph Problem›

text ‹
We shall prove 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."
›

theory Friends
  imports   Main 
            Finite_Set