theorem WrittenOnTheWallII.GraphConjecture6.conjecture6 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn : G.Connected) : 1 + G.n - G.m - G.a ≤ G.Ls

WOWII Conjecture 6

For a connected graph G we have Ls(G) ≥ 1 + n(G) - m(G) - a(G) where a(G) is defined via independent sets.