Theorem: Usa1998P1.zmod_eq (Compfiles/Usa1998P1.lean)

State before:
a b c : ℤ
⊢ a ≡ b [ZMOD c] ↔ a % c = b % c
Tactic:
rfl
State after:
no goals