chore: remove Ne.elim

[plp127]

This PR removes Ne.elim, as it is strictly less general than Not.elim. Dot notation will still work, since if we have h : a ≠ b then h.elim will elaborate to Not.elim h instead of Ne.elim h.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 49bb2031db89ba0405d44f7e8a439f96f459b287 --onto da19ea085d7cdba0131ec59b4f678b0910304878. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-09 19:03:34)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 49bb2031db89ba0405d44f7e8a439f96f459b287 --onto da19ea085d7cdba0131ec59b4f678b0910304878. You can force reference manual CI using the force-manual-ci label. (2026-07-09 19:03:35)