feat(data/finsupp/ne_locus): add a not-member lemma (#16245)
This PR adds a convenience lemma characterizing non-membership in the `ne_locus`.
`simp` proves this lemma, but given the position of the negations in `mem_ne_locus`, this form is also convenient.
