rw [← sum_add_distrib]
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
hB : B ⊆ A
⊢ ∑ v in C, degRes G v A = ∑ v in C, degRes G v B + ∑ v in C, degRes G v (A \ B)
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
hB : B ⊆ A
⊢ ∑ v in C, degRes G v A = ∑ x in C, (degRes G x B + degRes G x (A \ B))