Counting the connections left by path suppression

In a forest, two different intermediate vertices cannot give paths between the same endpoints. For a bipartition with degree at most two on the removed side, each removed degree-two vertex therefore gives exactly one distinct edge of the suppressed graph. Isolated vertices and leaves give no edges.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.Internal.exists_connection_equiv {V : Type} (B : SimpleGraph V) [Fintype V] (S : Finset V) (forest : B.IsAcyclic) (independent : ∀ u ∈ S, ∀ v ∈ S, ¬B.Adj u v) (coreIndependent : ∀ u ∉ S, ∀ v ∉ S, ¬B.Adj u v) (degree : ∀ v ∈ S, B.degree v ≤ 2) : ∃ (f : ↥({v ∈ S | B.degree v = 2}) ≃ ↑(graph B S).edgeSet), ∀ (x : ↥({v ∈ S | B.degree v = 2})), ∃ (u : { v : V // v ∉ S }) (v : { v : V // v ∉ S }), ↑(f x) = s(u, v) ∧ B.Adj ↑u ↑x ∧ B.Adj ↑x ↑v

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.Internal.edge_ncard_eq_degree_two {V : Type} (B : SimpleGraph V) [Fintype V] (S : Finset V) (forest : B.IsAcyclic) (independent : ∀ u ∈ S, ∀ v ∈ S, ¬B.Adj u v) (coreIndependent : ∀ u ∉ S, ∀ v ∉ S, ¬B.Adj u v) (degree : ∀ v ∈ S, B.degree v ≤ 2) : (graph B S).edgeSet.ncard = {v ∈ S | B.degree v = 2}.card