Theorem: Fin.prod_succ (GMLInit/Data/Fin/Basic.lean)

State before:
n : Nat
α : Type u_1
inst✝¹ : Mul α
inst✝ : OfNat α 1
f : Fin (n + 1) → α
⊢ prod f = f 0 * prod (f ∘ succ)
Tactic:
simp [prod, foldr_succ]
State after:
no goals