Spanning paths in connected graphs of degree at most two

A longest simple path cannot have an external neighbor at an endpoint. At an internal vertex its two path neighbors exhaust the ambient degree. Connectivity therefore forces the path to span the graph, including when the graph is a cycle. This supplies an ordering for the degree-two regions in Monien and Preis's thin-path argument.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_spanning_path {V : Type} [Fintype V] (B : SimpleGraph V) (connected : B.Connected) (degree : ∀ (v : V), B.degree v ≤ 2) : ∃ (u : V) (v : V) (p : B.Walk u v), p.IsPath ∧ ∀ (w : V), w ∈ p.support

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_spanning_path_in_region {V : Type} [Fintype V] (B : SimpleGraph V) {P : Finset V} (connected : (SimpleGraph.induce {v : V | v ∈ P} B).Connected) (degree : ∀ v ∈ P, B.degree v ≤ 2) : ∃ (u : V) (v : V) (p : B.Walk u v), p.IsPath ∧ p.support.toFinset = P