State the combinatorial results

Many results from [lectures 6 to 9](https://github.com/YaelDillies/maths-notes/blob/master/additive_combinatorics.pdf) are already in Mathlib and can readily be stated and proved from the Mathlib versions.