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

State before:
n : ℕ
⊢ ZMod.val [0]_(n + 1) = 0
Tactic:
rfl
State after:
no goals