Degree control under triangle peeling

Removing a triangle lowers each affected degree by at most two. When its three vertices have degree at least minDegree + 2, minimum degree is unchanged.

theorem LeanPool.DrossFractionalTriangleDecomposition.peeled_heavy_triangle_degree_add_two {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {u v w x : V} : G.degree x ≤ (G.deleteEdges ↑(triEdges {u, v, w})).degree x + 2

theorem LeanPool.DrossFractionalTriangleDecomposition.peeled_heavy_triangle_minDegree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {u v w : V} (hu : G.minDegree + 2 ≤ G.degree u) (hv : G.minDegree + 2 ≤ G.degree v) (hw : G.minDegree + 2 ≤ G.degree w) : (G.deleteEdges ↑(triEdges {u, v, w})).minDegree = G.minDegree