Theorem: cong_mod_n_equiv' (Instructor/Lectures/grad/sets_relations.lean)

State before:
⊢ ∀ (n : ℕ), Equivalence (cong_mod_n n)
Tactic:
intro n
State after:
n : ℕ
⊢ Equivalence (cong_mod_n n)