Theorem int.add_modeq_left

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