m n a b c d : ℤ
⊢ b % n = a % n ↔ n ∣ b - a
m n a b c d : ℤ
⊢ a ≡ b [ZMOD n] ↔ n ∣ b - a
rw [ModEq, eq_comm]
no goals
m n a b c d : ℤ
⊢ b % n = a % n ↔ n ∣ b - a
simp [emod_eq_emod_iff_emod_sub_eq_zero, dvd_iff_emod_eq_zero]