no goals
α : Type u_1
M : Type ?u.30419
N : Type u_2
P : Type ?u.30425
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂
simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _