The small-order Dross case

Below twenty vertices, the nine-tenths minimum-degree condition forces a nonempty graph to be complete. The empty graph has the trivial decomposition.

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

Dross's fractional triangle decomposition for graphs of order below twenty.