Algebraic connectivity of K_{2,n-2} equals 2

algConn_completeBipartite_two: the equality clause of the ACMAX conjecture. The Laplacian spectrum of K_{2,n-2} is 0, 2^(n-3), (n-2), n, so its second-smallest eigenvalue is 2.

theorem ACMax.algConn_completeBipartite_two (n : ℕ) (hn : 4 ≤ n) : algConn (completeBipartiteGraph (Fin 2) (Fin (n - 2))) = 2