exact card_disjoint_union (disj_of_inter_disj _ _ h)
α : 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
no goals