Theorem int.neg_modeq_neg

feat(data/{int,nat}/modeq): `a/c ≡ b/c mod m/c → a ≡ b mod m` (#18666) …