rw [degRes, nbhdRes,inter_distrib_right]
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
v : α
h : Disjoint A B
⊢ degRes G v (A ∪ B) = degRes G v A + degRes G v B
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
v : α
h : Disjoint A B
⊢ card (A ∩ neighborFinset G v ∪ B ∩ neighborFinset G v) = degRes G v A + degRes G v B