mathlib

bf7ef0e8 - feat(combinatorics/simple_graph/regularity): Increment partition (#19051)

feat(combinatorics/simple_graph/regularity): Increment partition (#19051) Define the increment partition and prove its two crucial properties: * It has size depending only on the size of the original partition * It increases the energy by a fixed amount This is all internal to the proof of SRL, so I made most lemmas `private`. Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>