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

State before:
m n k : ℕ
f : ℕ → ZMod m
⊢ prod_seq (n + 1) k f = prod_seq n k f * f (k + n)
Tactic:
rfl
State after:
no goals