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

State before:
m n : ℕ
f : ℕ → ZMod m
⊢ prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
Tactic:
rewrite [prod_seq_step, zero_add]
State after:
m n : ℕ
f : ℕ → ZMod m
⊢ prod_seq n 0 f * f n = prod_seq n 0 f * f n

State before:
m n : ℕ
f : ℕ → ZMod m
⊢ prod_seq n 0 f * f n = prod_seq n 0 f * f n
Tactic:
rfl
State after:
no goals