theorem WrittenOnTheWallII.GraphConjecture1.conjecture1 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn : G.Connected) : G.n + 1 - 2 * G.m ≤ G.Ls

WOWII Conjecture 1

For a simple connected graph G the maximum number of leaves of a spanning tree satisfies Ls(G) ≥ n(G) + 1 - 2·m(G) where n(G) counts vertices and m(G) is the size of a maximum matching.