feat(combinatorics/simple_graph): Mantel's theorem

[kmill]

If a graph has more than n^2/4 edges then it contains a triangle (Theorem I.2 of Bollobas, Modern Graph Theory). We should also eventually have Turán's theorem, which generalizes this.

---

[vihdzp]

Note: this is a special case of Turán's theorem. You could prove the stronger result that a graph with n vertices without a k-clique has at most vertices as the Turán graph.

[b-mehta]

Note: this is a special case of Turán's theorem. You could prove the stronger result that a graph with n vertices without a k-clique has at most vertices as the Turán graph.

Agreed, I had a go at this a while ago but since we didn't have API for cliques at the time it was pretty tricky, it might be more doable now!

[urkud]

Could you please change the title to be understandable without a textbook?

[YaelDillies]

I salvaged the code in LeanCamCombi. Note that I am also porting John Talbot's proof of Turan, so I am dropping the proof of Mantel here.