simp only [degRes_ones]
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
⊢ ∑ v in B, degRes G v (A \ B) = ∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
⊢ ∑ x in B, ∑ x in nbhdRes G x (A \ B), 1 = ∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0