Turán's Graph Theorem

Turán's Graph Theorem states that any undirected, simple graph with $n$ vertices that does not contain a $p$-clique, contains at most $\left( 1 - \frac{1}{p-1} \right) \frac{n^2}{2}$ edges. The theorem is an important result in graph theory and the foundation of the field of extremal graph theory. The formalisation follows Aigner and Ziegler's presentation in Proofs from THE BOOK of Turán's initial proof. Besides a direct adaptation of the textbook proof, a simplified, second proof is presented which decreases the size of the formalised proof significantly.