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

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