refactor(data/finsupp/ne_locus): Match `dist` API (#17036)
refactor(data/finsupp/ne_locus): Match `dist` API (#17036)

Rename `ne_locus` lemmas so they match the `dist` one. This is the name of them both being binary functions `f` such that `f a b = g (a - b)` for some `g`.





leanprover-community/mathlib,leanprover-community/mathlib