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

State before:
n : ℕ
L : List ℕ
⊢ prod (n :: L) = n * prod L
Tactic:
rfl
State after:
no goals