Theorem: HTPI.cc_eq_iff_congr (HTPILib/Chap7.lean)

State before:
m : ℕ
a b : ℤ
⊢ ↑m ∣ a - b ↔ a ≡ b (MOD m)
Tactic:
rfl
State after:
no goals