m n✝ a✝ b✝ c d a b n : ℤ
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t
m n✝ a✝ b✝ c d a b n : ℤ
⊢ a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
rw [modEq_iff_dvd]
no goals
m n✝ a✝ b✝ c d a b n : ℤ
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t
exact exists_congr fun t => sub_eq_iff_eq_add'