exact sum_union disjoint_sdiff
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
C : Finset α
⊢ ∑ v in B ∪ A \ B, degRes G v C = ∑ v in B, degRes G v C + ∑ v in A \ B, degRes G v C
no goals