mathlib3

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

feat(data/{int,nat}/modeq): `a/c ≡ b/c mod m/c → a ≡ b mod m` (#18666) Also prove `-a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]`, `a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]`, generalise `int.modeq.mul_left'`/`int.modeq.mul_right'`, and rename * `int.gcd_pos_of_non_zero_left` → `int.gcd_pos_of_ne_zero_left` * `int.gcd_pos_of_non_zero_right` → `int.gcd_pos_of_ne_zero_right` * `eq_iff_modeq_int`, `char_p.int_coe_eq_int_coe_iff` → `char_p.int_cast_eq_int_cast` (they were duplicates)