Commit 2023-04-02 23:06 47a1a733

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)