Commit 2023-05-19 22:52 bf7ef0e8

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.