feat(data/int|nat/modeq): add modneq notation

[oxarbitrage]

Add notation for ≢ in modeq files.

---

[eric-wieser]

I just have some formatting suggestions.

@eric-wieser I think a point in having modneq as a reducible definition is that it gives a way to have modneq-specific dot notation that falls back on not. It's similar to why neq exists.

Until we have such dot notation, I don't think there's any point introducing the name though.

[oxarbitrage]

@eric-wieser i removed the def as suggested. I think we need to keep the lemma but open to remove it if there are better alternatives to solve goals as:

example : 19 ≢ 6 [ZMOD 11] := by norm_num [modneq_iff]