no goals
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ 0 ≤ energy P G
refine' div_nonneg (Finset.sum_nonneg fun _ _ => sq_nonneg _) <| Nat.cast_nonneg _