Geometry of a peeled high-degree triangle

The three deleted pairs are genuine graph edges, are pairwise distinct, and deleting them lowers every degree by at most two.

theorem LeanPool.DrossFractionalTriangleDecomposition.heavy_triangle_vertices_distinct {V : Type u_1} (G : SimpleGraph V) {u v w : V} (huv : G.Adj u v) (huw : G.Adj u w) (hvw : G.Adj v w) : u ≠ v ∧ u ≠ w ∧ v ≠ w

theorem LeanPool.DrossFractionalTriangleDecomposition.triEdges_heavy_triangle_subset {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {u v w : V} (huv : G.Adj u v) (huw : G.Adj u w) (hvw : G.Adj v w) : triEdges {u, v, w} ⊆ G.edgeFinset

theorem LeanPool.DrossFractionalTriangleDecomposition.triEdges_heavy_triangle_card {V : Type u_1} (G : SimpleGraph V) [DecidableEq V] {u v w : V} (huv : G.Adj u v) (huw : G.Adj u w) (hvw : G.Adj v w) : (triEdges {u, v, w}).card = 3