theorem WrittenOnTheWallII.GraphConjecture4.conjecture4 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] [Nonempty α] (h_conn : G.Connected) : G.NG - 1 ≤ G.Ls

WOWII Conjecture 4

If G is a connected graph then the maximum number of leaves over all spanning trees satisfies Ls(G) ≥ NG(G) - 1 where NG(G) is the minimal neighbourhood size of a non-edge of G.