no goals
α : Type u_1
M : Type ?u.40308
N : Type u_2
P : Type ?u.40314
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f - g) f = g.support
rw [neLocus_comm, neLocus_self_sub_right]