have := _root_.sdiff_sdiff_eq_self hB
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
⊢ (∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0) = ∑ v in A \ B, degRes G v B
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0) = ∑ v in A \ B, degRes G v B