exact card_erase_of_mem (mem_sdiff.mpr ⟨hvA, hvB⟩)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
hvB : ¬v ∈ B
hvA : v ∈ A
⊢ card (erase (A \ B) v) = card (A \ B) - 1
no goals