Dross's fractional triangle decomposition theorem

If a finite graph has minimum degree at least nine tenths of its order, its edges admit an exact fractional decomposition into triangles. The proof peels high-degree triangles until the exact flow argument applies.

theorem LeanPool.DrossFractionalTriangleDecomposition.dross_fractional_flow_exact {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : 9 * Fintype.card V ≤ 10 * G.minDegree) : FractionalTriangleDecomp G

Dross's theorem at the exact 9/10 minimum-degree threshold.