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

State before:
a : ℤ
⊢ [a]_0 = a
Tactic:
rfl
State after:
no goals